From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Jul 2005 12:17:23 +0000 (+0000)
Subject: coercions are now stored in the .moo file.
X-Git-Tag: PRE_GETTER_STORAGE~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7916b85dd9dab26b628ace838c683beb31db9c1;p=helm.git

coercions are now stored in the .moo file.
---

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