X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=bae4a8f593628821b0f8d1181563aa7e496222b8;hb=8e6a30412bbac3acc0a020e0fe90d492b0fc6776;hp=088d1b69d690562e4ce74281f3109cccdee259d0;hpb=14724f9aab44f1b150a5509743a43cb6693d493e;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 088d1b69d..bae4a8f59 100644
--- 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: [
@@ -452,12 +452,17 @@ EXTEND
         id, Some typ
     | arg = single_arg -> arg, None
     | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, None, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
+    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [
@@ -491,11 +496,6 @@ EXTEND
         | _ -> failwith "Invalid index name."
     ]
   ];
-  induction_kind: [
-    [ "rec" -> `Inductive
-    | "corec" -> `CoInductive
-    ]
-  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -553,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 *)