]> matita.cs.unibo.it Git - helm.git/commitdiff
Serious bug fixed in simplify: sometimes terms wwere not closed because of
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Jul 2006 09:31:33 +0000 (09:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Jul 2006 09:31:33 +0000 (09:31 +0000)
the use of the wrong replace function (that did not perform the required lifting).

helm/software/components/tactics/proofEngineReduction.ml

index 1db075c70d96455a80c15ab49865eb3a02cde7be..6d198d4d133e721539c30e77d86196787ff6c1b5 100644 (file)
@@ -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 ****)