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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 695ef7a7f..f33c69e35 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -749,8 +749,10 @@ let fold term =
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*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
+   let replace =
+    ProofEngineReduction.replace
+     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~what:term' ~with_what:term
    in
     let ty' = replace ty in
     let context' =