X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;fp=helm%2FgTopLevel%2FproofEngine.ml;h=695ef7a7fbe31669813e2b5bc2b9b1ffcd48a78a;hb=9f45f8febfade5e1dca7a022154f2635be2af9b2;hp=42ee2c1609b9ab6d18a0f8bf30326c5cd326d930;hpb=2ef44e8d1a908a08d31e6114c15898ae7dc8109e;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 42ee2c160..695ef7a7f 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -750,7 +750,7 @@ let fold term =
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace = ProofEngineReduction.replace
-    ~equality:(==) ~what:term' ~with_what:term
+    ~equality:(=) ~what:term' ~with_what:term
    in
     let ty' = replace ty in
     let context' =