X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=f30a9fcb6ba34949c3ed99f1753a6e6607c820ed;hb=a99b3bf44964a6a3d56d752efbdc2c962ce24d08;hp=13b1d7270bc3fd1f785d8831a97ac284ec0b0bce;hpb=c6b50e06bd73a29501cafe599551db206193220b;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 13b1d7270..f30a9fcb6 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -49,9 +49,11 @@ let nparamod metasenv subst context t table =
   prerr_endline "Active table:";
   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
   let bag, maxvar, _, newclauses = 
-    Sup.superposition_right bag maxvar clause (active_clauses, table)
+    Sup.infer_right bag maxvar clause (active_clauses, table)
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+  prerr_endline "Proofs: ";
+  prerr_endline (Pp.pp_bag bag);
   prerr_endline "========================================";
 ;;