From 96fbcaa67d901a4ea0f2d06c624a4b1e83c0d5be 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). --- components/tactics/proofEngineReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml index 1db075c70..6d198d4d1 100644 --- a/components/tactics/proofEngineReduction.ml +++ b/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