Introduction of vectors of implicit (only for NG).

[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..27748245654989ef634ad940b51a6b026ec3f6c7 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)) ]
@@ -789,7 +789,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 +859,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 ->