X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=1b06b81c97fd64b26b4429956c25e9c573c7bdd5;hb=613077e2729b7a66cf10b4b930b431b73a0062c2;hp=e83152226f257cb21132fbb3abee6b0f3c271ae7;hpb=918b39ec5f3477499230c7370d4798f20a65cd8d;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e83152226..1b06b81c9 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -472,6 +472,8 @@ EXTEND
       body = term ->
         GrafiteAst.Obj (loc,
           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
+    | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
+        GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty =