X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=c1c7a9071fdee01ed9ad69959782f7e73886ad25;hb=33a4938d5ce3a5c240c0d35b6362c8072f8ba482;hp=6c6e07101249747aa8180ec1f464b466d843fe10;hpb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 6c6e07101..c1c7a9071 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -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 =