proofs are now built lazily at the end of the computation

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 42fc39bf31f2fb9694e5fa838ac814a684a28a51..74194e84a0f7aa678d36708d555299a86ef99ef8 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -6,9 +6,16 @@ type equality =
      Utils.comparison) * (* ordering *)  
     Cic.metasenv *       (* environment for metas *)
     Cic.term list        (* arguments *)
-;;
 
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+type proof =
+  | BasicProof of Cic.term
+  | ProofBlock of
+      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+        equality
+  | NoProof
+
+
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
 
 
 exception MatchingFailure
@@ -87,3 +94,10 @@ val fix_metas: int -> equality -> int * equality
 
 val extract_differing_subterms:
   Cic.term -> Cic.term -> (Cic.term * Cic.term) option
+
+
+val store_proof: equality -> proof -> unit
+
+val delete_proof: equality -> unit
+
+val build_term_proof: equality -> Cic.term