X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=0fc42291d318d76408280f51104c11340f7b5f23;hb=cd415135f0bcf53f10ed7649fcacc3247bc7a3f1;hp=52f151fc274a59a8dca825506429c10d9f051c20;hpb=bee436af0c6ceb1c83259c94036df8b12f901f2d;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 52f151fc2..0fc42291d 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -95,7 +95,7 @@ let mk_rec_corec ind_kind defs loc =
    else
     `MutualDefinition
   in
-   (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body))))
+   (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
 
 let nmk_rec_corec ind_kind defs loc = 
  let loc,t = mk_rec_corec ind_kind defs loc in
@@ -797,12 +797,16 @@ EXTEND
       IDENT "nqed" -> G.NQed loc
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        G.NObj (loc, N.Theorem (nflavour, name, typ, body))
+        G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
-        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
+        G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
-        G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+        G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
+    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
+      paramspec = OPT inverter_param_list ; 
+      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
+        G.NInverter (loc,name,indty,paramspec,outsort)
     | NLETCOREC ; defs = let_defs -> 
         nmk_rec_corec `CoInductive defs loc
     | NLETREC ; defs = let_defs -> 
@@ -852,16 +856,16 @@ EXTEND
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
         G.Obj (loc, 
           N.Theorem 
-            (`Variant,name,typ,Some (N.Ident (newname, None))))
+            (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        G.Obj (loc, N.Theorem (flavour, name, typ, body))
+        G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
         G.Obj (loc,
-          N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
+          N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
-        G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
+        G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
     | LETCOREC ; defs = let_defs -> 
         mk_rec_corec `CoInductive defs loc
     | LETREC ; defs = let_defs ->