X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=5906bc06d3989b27c629a8ef4bbf8a952ec85313;hb=4f3b04e9966484011328d5b0eb358da4416e29b0;hp=0f92c66209f08838469c5ded84e0284ad56b1005;hpb=d0d2ebcf0ad48c38dcd69142f5e080e987fc5536;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml
index 0f92c6620..5906bc06d 100644
--- a/matitaB/components/ng_paramodulation/nCicParamod.ml
+++ b/matitaB/components/ng_paramodulation/nCicParamod.ml
@@ -92,14 +92,17 @@ module P = NCicParamod
 type state = P.state
 let empty_state = P.empty_state
 
+let size_of_state = P.size_of_state
+
 let forward_infer_step status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let saturate (t,ty) = 
     NCicBlob.saturate status metasenv subst context t ty in
-  let bag,clause = P.mk_passive bag (t,ty) in
+  let bag,clause = P.mk_passive bag (saturate (t,ty)) in
     if Terms.is_eq_clause clause then
-      P.forward_infer_step (P.replace_bag s bag) clause 0
-    else (debug (lazy "not eq"); s)
+      ((*prerr_endline "is eq";*)
+      P.forward_infer_step (P.replace_bag s bag) clause 0)
+    else ((*print (lazy "not eq");*) s)
 ;;
 
 let index_obj status s uri =
@@ -152,7 +155,7 @@ let is_equation status metasenv subst context ty =
     NCicMetaSubst.saturate status ~delta:0 metasenv subst context
       ty 0 
   in match hty with
-    | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
+    | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true
     | _ -> false
 ;;