X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.mli;h=821ac0e2cbb8f08ef0255ec3e6c47771df2bebdb;hb=c091ca7a030a85a529543de98e45c54284028b63;hp=5ba90f943d9bcb49f1f83f78fd7905f2b6f22f5d;hpb=4ae7d510a430a2a6929f973d36b993d528772d64;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 5ba90f943..821ac0e2c 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -1,4 +1,5 @@
 val nparamod : 
+  #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
-     unit
+     NCic.term * NCic.metasenv * NCic.substitution