From: Claudio Sacerdoti Coen Date: Wed, 16 May 2012 20:21:59 +0000 (+0000) Subject: Compare was not compatible with eq! X-Git-Tag: make_still_working~1731 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d2ded02c4252d3db0a9f5249d5b5d0f84f48d04;p=helm.git Compare was not compatible with eq! The first used alpha_eq, the second did not. Now both do. --- diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml index b9314a203..9e17f86d5 100644 --- a/matita/components/ng_paramodulation/nCicBlob.ml +++ b/matita/components/ng_paramodulation/nCicBlob.ml @@ -45,8 +45,10 @@ with type t = NCic.term and type input = NCic.term = struct type t = NCic.term - let eq x y = x = y;; - (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *) + let eq x y = + (* CSC: NCicPp.status is the best I can put here *) + x = y || + NCicReduction.alpha_eq (new NCicPp.status) C.metasenv C.subst C.context x y;; let height_of_ref = function | NReference.Def h -> h @@ -79,9 +81,7 @@ with type t = NCic.term and type input = NCic.term = struct ;; let compare x y = - (* CSC: NCicPp.status is the best I can put here *) - if NCicReduction.alpha_eq (new NCicPp.status) [] [] [] x y then 0 - (* if x = y then 0 *) + if eq x y then 0 else compare x y ;;