compact coercion command: "coercion foo."

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

diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml
index 9d4d3490a9ce7b3729b85e50484bf3790b174ad2..0db31e94dd9e104cc754196796353c7f1eee0cec 100644 (file)
--- a/matitaB/components/grafite/grafiteAst.ml
+++ b/matitaB/components/grafite/grafiteAst.ml
@@ -103,8 +103,8 @@ type command =
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *
-      NotationPt.term * NotationPt.term *
-      (string * NotationPt.term) * NotationPt.term
+      (NotationPt.term * NotationPt.term *
+        (string * NotationPt.term) * NotationPt.term) option
   | NQed of loc
   (* ex lexicon commands *)
   | Alias of loc * alias_spec