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/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 1db075c70d96455a80c15ab49865eb3a02cde7be..6d198d4d133e721539c30e77d86196787ff6c1b5 100644 (file)
--- 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 ****)