From 707c29a9125acc5b1b1fdee6e93ca551744ba946 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Jul 2006 09:31:33 +0000 Subject: [PATCH] Serious bug fixed in simplify: sometimes terms wwere not closed because of the use of the wrong replace function (that did not perform the required lifting). --- helm/software/components/tactics/proofEngineReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 1db075c70..6d198d4d1 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -859,7 +859,7 @@ let simpl context = let simplified_term_to_fold = reduceaux context [] delta_expanded_term_to_fold in - replace (=) [simplified_term_to_fold] [term_to_fold] res + replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res with WrongShape -> (**** Step 3.2 ****) -- 2.39.2