X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineReduction.ml;h=6d198d4d133e721539c30e77d86196787ff6c1b5;hb=3c1f5f810ce2acbbfc6e8f5d50e22bd4068b09a7;hp=1db075c70d96455a80c15ab49865eb3a02cde7be;hpb=b52068a8a5d0af94ad09c93ae63aed3424fbb924;p=helm.git

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