From 00affce1439533d9b7e581947cefdff93a71ea7b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 14:52:17 +0000 Subject: [PATCH] Signature and concrete syntax of fold fixed. --- helm/matita/matitaEngine.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 1718529cc..2a73193f6 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -46,7 +46,7 @@ let tactic_of_ast = function | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Exists _ -> Tactics.exists | TacticAst.Fail _ -> Tactics.fail - | TacticAst.Fold (_, reduction_kind, pattern) -> + | TacticAst.Fold (_, reduction_kind, term, pattern) -> let reduction = match reduction_kind with | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] @@ -54,7 +54,7 @@ let tactic_of_ast = function | `Simpl -> ProofEngineReduction.simpl | `Whd -> CicReduction.whd ~delta:false ~subst:[] in - Tactics.fold ~reduction ~pattern + Tactics.fold ~reduction ~term ~pattern | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.FwdSimpl (_, hyp, names) -> Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ()) @@ -441,9 +441,10 @@ let disambiguate_tactic status = function status, TacticAst.ElimType (loc, cic) | TacticAst.Exists loc -> status, TacticAst.Exists loc | TacticAst.Fail loc -> status,TacticAst.Fail loc - | TacticAst.Fold (loc,reduction_kind, pattern) -> + | TacticAst.Fold (loc,reduction_kind, term, pattern) -> let status, pattern = disambiguate_pattern status pattern in - status, TacticAst.Fold (loc,reduction_kind, pattern) + let status, term = disambiguate_term status term in + status, TacticAst.Fold (loc,reduction_kind, term, pattern) | TacticAst.FwdSimpl (loc, hyp, names) -> status, TacticAst.FwdSimpl (loc, hyp, names) | TacticAst.Fourier loc -> status, TacticAst.Fourier loc -- 2.39.2