X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fequality.mli;h=1182afee654d855ea8bda55f5a5914d1dd10cf5a;hb=54632bfcefb8f9cf2265b27196207b2786e84927;hp=237045bec67722aa241333d0e6f0f9a644f90057;hpb=218d9cfaa1e2874b62c3e08adf98c4f9a85d2c11;p=helm.git

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 237045bec..1182afee6 100644
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -108,3 +108,14 @@ val symmetric:
   Cic.term -> Cic.term -> int -> UriManager.uri ->
     Cic.metasenv -> proof
 
+(* takes 3 lists of alive ids (they are threated the same way, the type is
+ * funny just to not oblige you to concatenate them) and drops all the dead
+ * equalities *)
+val collect: int list -> int list -> int list -> unit
+
+(* given an equality, returns the numerical id *)
+val id_of: equality -> int
+
+(* profiling statistics *)
+val get_stats: unit -> string
+