coercions are now stored in the .moo file.

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5e3e336060bb8c15b9ad8faecf0d56ad8bd114cb..df8f484ba211a6f327614e805cd8f9f7d1ae19cf 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -257,7 +257,12 @@ let eval_command status cmd =
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj status
   | TacticAst.Coercion (loc, coercion) -> 
-      eval_coercion status coercion
+      let status = eval_coercion status coercion in
+      let moo_content_rev =
+       (TacticAstPp.pp_cic_command
+         (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
+       status.moo_content_rev in
+      {status with moo_content_rev = moo_content_rev}
   | TacticAst.Alias (loc, spec) -> 
      let aliases =
       match spec with