From 86a273d0b145e058baf50b6e97fcb0dc0adc90e3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 18 Dec 2009 08:52:16 +0000 Subject: [PATCH] using = instead of alpha conversions. context metasenv and subst are not needed any more --- helm/software/components/ng_paramodulation/nCicBlob.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index b02a1ebc0..4c3c13205 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -45,7 +45,8 @@ with type t = NCic.term and type input = NCic.term = struct type t = NCic.term - let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; + let eq x y = x = y;; + (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *) let rec compare x y = match x,y with @@ -63,7 +64,8 @@ with type t = NCic.term and type input = NCic.term = struct ;; let compare x y = - if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 + (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 *) + if x = y then 0 else compare x y ;; -- 2.39.2