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 b02a1ebc0b4cadb1614a44f46971d601ccc6170b..4c3c1320558f39f424a0c510d21404608ae675cb 100644 (file)
--- 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
   ;;