compact coercion command: "coercion foo."

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

diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index 30a97a3e3e130a28aee11926b17ce043b80dc48e..3e77258e0f0e2843d20dc98f0f0c96ac3190de3b 100644 (file)
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -221,7 +221,7 @@ EXTEND
                 G.NMacro(loc,
              G.NAutoInteractive (loc, (None,["depth",depth]@params))))
     | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc)
-    | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
+    | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t))
     | IDENT "screenshot"; fname = QSTRING -> 
         G.NMacro(loc,G.Screenshot (loc, fname))
     | IDENT "cases"; what = tactic_term ; where = pattern_spec ->
@@ -576,11 +576,11 @@ EXTEND
          G.NUnivConstraint (loc,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
-    | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term; 
+    | IDENT "coercion"; name = IDENT; spec = OPT [ SYMBOL ":"; ty = term; 
         SYMBOL <:unicode<def>>; t = term; "on"; 
         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
-        "to"; target = term ->
-          G.NCoercion(loc,name,t,ty,(id,source),target)     
+        "to"; target = term -> t,ty,(id,source),target ] ->
+        G.NCoercion(loc,name,spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
     | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with";