From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Dec 2011 08:43:55 +0000 (+0000)
Subject: axiom-
X-Git-Tag: make_still_working~2018
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f973cb2c6d6f7fffc5e3263fe5acc5507292458e;p=helm.git

axiom-
---

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 ;