From f973cb2c6d6f7fffc5e3263fe5acc5507292458e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Dec 2011 08:43:55 +0000 Subject: [PATCH] axiom- --- matita/components/grafite_parser/grafiteParser.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 376c5c9cc..c21457ad6 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -501,7 +501,7 @@ EXTEND loc,path,G.WithoutPreferences ]]; - index: [[ b = OPT SYMBOL "-" -> match b with None -> false | _ -> true ]]; + index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]]; grafite_ncommand: [ [ IDENT "qed" ; i = index -> G.NQed (loc,i) @@ -513,7 +513,7 @@ EXTEND G.NObj (loc, N.Theorem(nflavour, name, N.Implicit `JustOne, Some body,`Regular), true) - | i = index; IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> + | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term -> G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i) | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; -- 2.39.2