CProp hierarchy is there!

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 461e2fc9f755e9b0f868188ac4b535accd4b996d..bae4a8f593628821b0f8d1181563aa7e496222b8 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -427,7 +427,7 @@ EXTEND
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
@@ -496,11 +496,6 @@ EXTEND
         | _ -> failwith "Invalid index name."
     ]
   ];
-  induction_kind: [
-    [ "rec" -> `Inductive
-    | "corec" -> `CoInductive
-    ]
-  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -558,9 +553,12 @@ EXTEND
     [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
-    | "let"; k = induction_kind; defs = let_defs; "in";
+    | LETCOREC; defs = let_defs; "in";
+      body = term ->
+        return_term loc (Ast.LetRec (`CoInductive, defs, body))
+    | LETREC; defs = let_defs; "in";
       body = term ->
-        return_term loc (Ast.LetRec (k, defs, body))
+        return_term loc (Ast.LetRec (`Inductive, defs, body))
     ]
   ];
   term: LEVEL "20R"  (* binder *)