From 9f45f8febfade5e1dca7a022154f2635be2af9b2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 May 2002 15:48:48 +0000 Subject: [PATCH] Fold must use replace with the = equality and not the physical == equality. --- helm/gTopLevel/proofEngine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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' = -- 2.39.2