From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jul 2006 09:31:33 +0000 (+0000)
Subject: Serious bug fixed in simplify: sometimes terms wwere not closed because of
X-Git-Tag: 0.4.95@7852~1185
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=96fbcaa67d901a4ea0f2d06c624a4b1e83c0d5be;p=helm.git

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).
---

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 ****)