From 9d2ded02c4252d3db0a9f5249d5b5d0f84f48d04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 May 2012 20:21:59 +0000 Subject: [PATCH] Compare was not compatible with eq! The first used alpha_eq, the second did not. Now both do. --- matita/components/ng_paramodulation/nCicBlob.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 ;; -- 2.39.2