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 =