Active goals are now demodulated after selecting a positive clause.

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

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 78bea9934c540d3936d4a73ae4a09ac03dfc5658..5ba90f943d9bcb49f1f83f78fd7905f2b6f22f5d 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -1,4 +1,4 @@
 val nparamod : 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
-    NCic.term -> NCic.term list ->
+    (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
      unit