short notation for "coercion"

[helm.git] / matita / components / grafite / grafiteAst.ml

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e96cf1bbcb8b9cf04b28f14c61613c9cdcaee9a3..2d55e8634fd73bd88b44ee9ede5ae07e158ad84e 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -104,7 +104,8 @@ type command =
   | NInverter of loc * string * nterm * bool list option * nterm option
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
-  | NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm
+  | NCoercion of loc * string * bool * 
+      (nterm * nterm * (string * nterm) * nterm) option
   | NQed of loc * bool
   (* ex lexicon commands *)
   | Alias of loc * alias_spec