X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=64d68a37e53adc2aa635bd2b77fd31dea6c254c1;hb=c7eb56246dc1199f098ed6c8c77aa08fea9a62f8;hp=0885f3037ffdcc1dfb9493ec1214f22f09b77022;hpb=5dac9432fa233251332953770319c0b95984e1c5;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 0885f3037..64d68a37e 100644
--- 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