freescale porting

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

diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli
index 4383b2928956ada851ae6de53b87a68454ccf915..1ba93353b4f646abe3069aff5deac5c661c219c2 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.mli
+++ b/helm/software/components/ng_paramodulation/nCicProof.mli
@@ -22,4 +22,4 @@ val mk_proof:
   -> Terms.M.key 
   -> NCic.term Terms.substitution
   -> Terms.M.key list 
-  -> NCic.term
+  -> NCic.term * NCic.term (* proof, type *)