The Blob is not abstracted on the context any more.

[helm.git] / matitaB / components / ng_paramodulation / paramod.ml

diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml
index 86a964c1487f36a7f72deb0c8f2608f621ec2aac..33f802f7f036caf9152d65de93a4c3cabce55842 100644 (file)
--- a/matitaB/components/ng_paramodulation/paramod.ml
+++ b/matitaB/components/ng_paramodulation/paramod.ml
@@ -208,16 +208,17 @@ module Paramod (B : Orderings.Blob) = struct
     (bag, maxvar), c
   ;;
 
-  let mk_clause bag maxvar (t,ty) =
-    let (proof,ty) = B.saturate t ty in
+(*
+  let mk_clause bag maxvar (proof,ty) =
+    let (proof,ty) = B.saturate t ty in 
     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
     let bag, c = Terms.add_to_bag c bag in
     (bag, maxvar), c
-  ;;
+  ;; *)
   
-  let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+  let mk_passive (bag,maxvar) = mk_unit_clause bag maxvar;;
 
-  let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+  let mk_goal (bag,maxvar) = mk_unit_clause bag maxvar;;
 
   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
     let (bag,maxvar), g = mk_unit_clause bag maxvar t in