now the moo contains also composed coercions (and It should prevent

the .moo user to recreate them)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5919a7bfc696f0fa05f16accf153b0f55397dd84..0e46c34d2236549a834ee624b2f11c353f4f1ea8 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -179,6 +179,21 @@ let eval_coercion status coercion =
   let status =
    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
     status new_coercions in
+  let statement_of name =
+    TacticAstPp.pp_statement 
+      (TacticAst.Executable (CicAst.dummy_floc,
+        (TacticAst.Command (CicAst.dummy_floc,
+          (TacticAst.Coercion (CicAst.dummy_floc, 
+            (CicAst.Ident (name, None)))))))) ^ "\n"
+  in
+  let moo_content_rev =
+    [statement_of (UriManager.name_of_uri coer_uri)] @ 
+    (List.map 
+      (fun (uri, _, _) -> 
+        statement_of (UriManager.name_of_uri uri))
+    new_coercions) @ status.moo_content_rev 
+  in
+  let status =  {status with moo_content_rev = moo_content_rev} in
   {status with proof_status = No_proof}
 
 let generate_elimination_principles uri status =
@@ -257,12 +272,7 @@ let eval_command status cmd =
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       MatitaSync.add_obj uri obj status
   | TacticAst.Coercion (loc, 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}
+      eval_coercion status coercion
   | TacticAst.Alias (loc, spec) -> 
      let aliases =
       match spec with