From: Claudio Sacerdoti Coen Date: Tue, 28 May 2002 15:48:48 +0000 (+0000) Subject: Fold must use replace with the = equality and not the physical == equality. X-Git-Tag: V_0_3_0_debian_8~72 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f45f8febfade5e1dca7a022154f2635be2af9b2;p=helm.git Fold must use replace with the = equality and not the physical == equality. --- 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' =