labels here and there

[helm.git] / helm / ocaml / tactics / paramodulation / inference.mli

diff --git a/helm/ocaml/tactics/paramodulation/inference.mli b/helm/ocaml/tactics/paramodulation/inference.mli
index 30927dc72d4e7a9c3eb3836d23bdc1a0358303f1..fde29e3527685bfe49a7265ec4c98303f590ffa5 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.mli
+++ b/helm/ocaml/tactics/paramodulation/inference.mli
@@ -34,7 +34,7 @@ type equality =
     Cic.term list        (* arguments *)
 
 and proof =
-  | NoProof
+  | NoProof   (* no proof *)
   | BasicProof of Cic.term (* already a proof of a goal *)
   | ProofBlock of (* proof of a rewrite step *)
       Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
@@ -48,7 +48,7 @@ and proof =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
 
 (** builds the Cic.term encoded by proof *)
-val build_proof_term: proof -> Cic.term
+val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string