new macro ncheck. fixed term2pres for Inductive and LetIn=Cast

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 5ed2939488b82f7355296f08a26c01a3686f52c2..c92e3175f45d9f84d80aa4c88df4272db669a2bb 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -79,7 +79,7 @@ let mk_rec_corec ind_kind defs loc =
   let name,ty = 
     match defs with
     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
-        let ty = match ty with Some ty -> ty | None -> N.Implicit in
+        let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
         let ty =
          List.fold_right
           (fun var ty -> N.Binder (`Pi,var,ty)
@@ -209,11 +209,11 @@ EXTEND
       let deannotate = function
         | N.AttributedTerm (_,t) | t -> t
       in match deannotate params with
-      | N.Implicit -> [false]
+      | N.Implicit _ -> [false]
       | N.UserInput -> [true]
       | N.Appl l -> 
          List.map (fun x -> match deannotate x with  
-           | N.Implicit -> false
+           | N.Implicit _ -> false
            | N.UserInput -> true
            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
@@ -652,6 +652,11 @@ EXTEND
         in
         (params,name,typ,fields)
     ] ];
+
+    nmacro: [
+      [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+      ]
+    ];
     
     macro: [
       [ [ IDENT "check"   ]; t = term ->
@@ -789,7 +794,7 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
-        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
+        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
     | NLETCOREC ; defs = let_defs -> 
@@ -859,7 +864,7 @@ EXTEND
     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
         G.Obj (loc,
-          N.Theorem (flavour, name, N.Implicit, Some body))
+          N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
     | LETCOREC ; defs = let_defs -> 
@@ -938,6 +943,7 @@ EXTEND
         punct = punctuation_tactical ->
           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
+    | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
     ]
   ];
   comment: [