Fixed wrong types in proof terms

[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 69299b13fd1d6e1fa2ed70d22ab213822860a0f8..821ac0e2cbb8f08ef0255ec3e6c47771df2bebdb 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -2,4 +2,4 @@ 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