]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/paramod.mli
1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
[helm.git] / helm / software / components / ng_paramodulation / paramod.mli
index db112450d8b0503079a63167e10839e12c5c4236..5ba90f943d9bcb49f1f83f78fd7905f2b6f22f5d 100644 (file)
@@ -1 +1,4 @@
-val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> unit
+val nparamod : 
+  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+    (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
+     unit