- bug fixed: some liftings were missing in the implementation of rewrite

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 0885f3037ffdcc1dfb9493ec1214f22f09b77022..64d68a37e53adc2aa635bd2b77fd31dea6c254c1 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -224,7 +224,8 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace =
     ProofEngineReduction.replace
-     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~equality:
+      (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
      ~what:term' ~with_what:term
    in
     let ty' = replace ty in