From e7916b85dd9dab26b628ace838c683beb31db9c1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 12:17:23 +0000
Subject: [PATCH] coercions are now stored in the .moo file.

---
 helm/matita/matitaEngine.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5e3e33606..df8f484ba 100644
--- 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
-- 
2.39.2