X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.mli;h=74194e84a0f7aa678d36708d555299a86ef99ef8;hb=e67aacd065c5f2bb90dc6b07850b4f4c2bc865fc;hp=0cc0fcb708d9f51be2a844a04fece6b5656e433a;hpb=423f3f23abfe6d5906818c26ab92d3703714057d;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 0cc0fcb70..74194e84a 100644
--- 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
@@ -18,7 +25,12 @@ val matching:
   CicUniv.universe_graph ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+val unification:
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  CicUniv.universe_graph ->
+  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+    
 (**
    Performs the beta expansion of the term "where" w.r.t. "what",
    i.e. returns the list of all the terms t s.t. "(t what) = where".
@@ -79,3 +91,13 @@ val subsumption: environment -> equality -> equality -> bool
 val metas_of_term: Cic.term -> int list
 
 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