...

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e83152226f257cb21132fbb3abee6b0f3c271ae7..1b06b81c97fd64b26b4429956c25e9c573c7bdd5 100644 (file)
--- 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 =