X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=fb9ee62457b2c2e20257ac08368ac4f09fffa6f1;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=c1c7a9071fdee01ed9ad69959782f7e73886ad25;hpb=12f96bd48b460d06f9858a334ee7c52d6831712f;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index c1c7a9071..fb9ee6245 100644
--- 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
   ;;