From e7916b85dd9dab26b628ace838c683beb31db9c1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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