Added initial support for inversion principles in Matita 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 52f151fc274a59a8dca825506429c10d9f051c20..8a418200d94604127cd7aad3a000aafdca921417 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -803,6 +803,8 @@ EXTEND
         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))
+    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term -> 
+        G.NInverter (loc,name,indty)
     | NLETCOREC ; defs = let_defs -> 
         nmk_rec_corec `CoInductive defs loc
     | NLETREC ; defs = let_defs ->