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 d110bda9a65d10b6cabfc0074a798e5bd7040786..bae4a8f593628821b0f8d1181563aa7e496222b8 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -224,7 +224,7 @@ let level_of precedence associativity =
   in
   string_of_int precedence ^ assoc_string
 
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23
@@ -427,7 +427,7 @@ EXTEND
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
@@ -457,10 +457,12 @@ EXTEND
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, None, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
-    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
+    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [
@@ -494,11 +496,6 @@ EXTEND
         | _ -> failwith "Invalid index name."
     ]
   ];
-  induction_kind: [
-    [ "rec" -> `Inductive
-    | "corec" -> `CoInductive
-    ]
-  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -556,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 *)