demo_works

examples/BasicDemos/Demo.ml

@@ -391,14 +391,19 @@ type typereca1 = | Typereca_1 of typereca2
       on the fly into a coq mutual inductive
 type typerecb1 = | Typerecb_1 of typerecb2
  and typerecb2 = { typerecb_2 : typerecb1 }
+
+  --> the work around is to break circularity using polymorphism, e.g.:
 *)
 
+type 'a typerecb2 = { typerecb_2 : 'a }
+type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
+
 (* not supported: recursive definitions using abbreviation
 
 type typerecb1 = | Typerecb_1 of typerecb2
  and typerecb2 = typerecb1 list
 
-   work around by inlining, e.g.:
+   --> the work around by inlining, e.g.:
 *)
 
 type typerecc1 = | Typerecc_1 of typerecc1 list