lexicon commands must tbe parsed before grafite commands rather than

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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index fd9c2946d9476a956821248b07f0ee3deaa15042..25024f26d4970c8bf45acf853f5d031425b775ed 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -505,7 +505,8 @@ EXTEND
   ]];
 
   grafite_ncommand: [ [
-      IDENT "qed" ;  i = index -> G.NQed (loc,i)
+      lc = lexicon_command -> lc
+    | IDENT "qed" ;  i = index -> G.NQed (loc,i)
     | IDENT "defined" ;  i = index -> G.NQed (loc,i) (* FG: presentational qed for definitions *)
     | src = source; nflavour = ntheorem_flavour; name = IDENT;
       params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term; (* FG: params added *)
@@ -576,7 +577,6 @@ EXTEND
       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
         G.NCopy (loc,s,NUri.uri_of_string u,
           List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
-    | lc = lexicon_command -> lc
   ]];
 
   lexicon_command: [ [