fix

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

diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli
index b31d8bacff7dc10b2f69eb5427f53498afdae7fa..5fdf694fc01f4d4777820e979a418891602af593 100644 (file)
--- a/components/tactics/paramodulation/inference.mli
+++ b/components/tactics/paramodulation/inference.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+val metas_of_proof_time : float ref
+
 type equality =
     int *                (* weight *)
     proof *              (* proof *)
@@ -52,11 +54,13 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string
 
+val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+
 exception MatchingFailure
 
 (** matching between two terms. Can raise MatchingFailure *)
 val matching:
-  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
@@ -65,7 +69,7 @@ val matching:
    such case should be significantly faster than CicUnification.fo_unif
 *)
 val unification:
-  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
@@ -129,6 +133,7 @@ val is_identity: environment -> equality -> bool
 val string_of_equality: ?env:environment -> equality -> string
 
 val metas_of_term: Cic.term -> int list
+val metas_of_proof: proof -> int list
 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality