From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 18 Dec 2009 08:52:16 +0000 (+0000)
Subject: using = instead of alpha conversions. context metasenv and subst are not
X-Git-Tag: make_still_working~3163
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=86a273d0b145e058baf50b6e97fcb0dc0adc90e3;p=helm.git

using = instead of alpha conversions. context metasenv and subst are not
needed any more
---

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
   ;;