new paramodulation

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 4bb43ea8fa2761538273c750d5d7f7896445b0e4..d0556dd5444b1fbf52bb6e9db227f0fe073687b0 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -19,7 +19,7 @@ and proof =
         (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof (* equality *)
   | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
-
+  | SubProof of Cic.term * int * proof
 
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
 
@@ -55,7 +55,7 @@ val beta_expand:
 *)
 val find_equalities:
   ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
-  equality list * int
+  int list * equality list * int
 
 
 exception TermIsNotAnEquality;;
@@ -105,8 +105,17 @@ val fix_metas: int -> equality -> int * equality
 val extract_differing_subterms:
   Cic.term -> Cic.term -> (Cic.term * Cic.term) option
 
-val build_proof_term: equality -> Cic.term
+val build_proof_term: proof (* equality *) -> Cic.term
 
 val find_library_equalities:
-  dbd:HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
-  equality list * int
+  HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+  UriManager.UriSet.t * equality list * int
+
+val find_library_theorems:
+  HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
+  (Cic.term * Cic.term * Cic.metasenv) list
+
+val find_context_hypotheses:
+  environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
+
+val string_of_proof: proof -> string