Extended the equality case to non ground terms

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

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index fb93ec7f84edb4d70e3f14c0e0270f2d15ce4545..13b1d7270bc3fd1f785d8831a97ac284ec0b0bce 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -48,8 +48,8 @@ let nparamod metasenv subst context t table =
   in
   prerr_endline "Active table:";
   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
-  let bag, maxvar, newclauses = 
-    Sup.superposition_right_with_table bag maxvar clause table
+  let bag, maxvar, _, newclauses = 
+    Sup.superposition_right bag maxvar clause (active_clauses, table)
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;