various updates, removed proofs for now because they are the real bottleneck!!

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 5ced528bb81055550961d65e489068bded9c49cf..42fc39bf31f2fb9694e5fa838ac814a684a28a51 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -18,7 +18,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".