moved coercion to library (work in progress)

[helm.git] / helm / ocaml / grafite / grafiteAst.ml

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index 2058ba37aae5f5496de0726ba408f0359c5c2114..f3687789b4ffef162f9c341c14fae13008529b9a 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -124,7 +124,7 @@ let eq_metadata = (=)
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 2
+let magic = 3
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -135,7 +135,7 @@ type ('term,'obj) command =
       (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Coercion of loc * 'term
+  | Coercion of loc * 'term * bool (* add composites *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj