From fe8280699be02d612da06ec67c7b79bb8b0a2bb6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 5 Jul 2005 14:27:16 +0000
Subject: [PATCH] now the moo contains also composed coercions (and It should
 prevent the .moo user to recreate them)

---
 helm/matita/matitaEngine.ml | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5919a7bfc..0e46c34d2 100644
--- 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
-- 
2.39.2