λδ site update

[helm.git] / helm / software / components / ng_paramodulation / nCicBlob.ml

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 6c6e07101249747aa8180ec1f464b466d843fe10..fb9ee62457b2c2e20257ac08368ac4f09fffa6f1 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -91,8 +91,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 x = y  then 0
+    if NCicReduction.alpha_eq [] [] [] x y  then 0 
+    (* if x = y  then 0 *)
     else compare x y
   ;;
 
@@ -101,10 +101,11 @@ with type t = NCic.term and type input = NCic.term = struct
 
   let is_eq = function
     | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
-        Some (ty,l,r)
+        Some (ty,l,r) 
+(*
     | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
        when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
-        Some (ty,l,r)
+        Some (ty,l,r) *)
     | _ -> None
 
   let pp t =