X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicParamod.mli;h=a0f5265eea85c4798bdbefb1f9f1a5dc17da4b7d;hb=9c21f4a9a35415878189aca003847cbd42c1a9fc;hp=0572f8c64ea74ddf6bf15b7813e901f5e6648d32;hpb=21ee96d317a4f0e7abfe76f697defe78acc10b94;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli
index 0572f8c64..a0f5265ee 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.mli
+++ b/helm/software/components/ng_paramodulation/nCicParamod.mli
@@ -15,7 +15,7 @@ val nparamod :
   #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
-     (NCic.term * NCic.metasenv * NCic.substitution) list
+     (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
 
 type state 
 val empty_state: state
@@ -26,4 +26,4 @@ val fast_eq_check :
   NCic.metasenv -> NCic.substitution -> NCic.context ->
   state -> 
   (NCic.term * NCic.term) -> 
-  (NCic.term * NCic.metasenv * NCic.substitution) list
+  (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list