X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Findexing.mli;h=fe8582e92dc21788252f83ec2c678e18db9cf409;hb=356f9fafa095801f1be70ff495f0977ce96ed6bc;hp=27ac1680a72c8b0231f61367a68c124d3c42ab1c;hpb=25835a1eac5698fedca50ebae1e18bef49a67c87;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index 27ac1680a..fe8582e92 100644
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -40,11 +40,7 @@ val index : Index.t -> Equality.equality -> Index.t
 val remove_index : Index.t -> Equality.equality -> Index.t
 val in_index : Index.t -> Equality.equality -> bool
 val empty : Index.t
-val match_unif_time_ok : float ref
-val match_unif_time_no : float ref
-val indexing_retrieval_time : float ref
 val init_index : unit -> unit
-val build_newtarget_time : float ref
 val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -62,6 +58,7 @@ val superposition_left :
    goal list
 
 val superposition_right :
+  ?subterms_only:bool ->
   int ->
   'a * Cic.context * CicUniv.universe_graph ->
   Index.t ->
@@ -89,3 +86,5 @@ val check_target:
   Cic.context ->
     Equality.equality -> string -> unit
 
+    (** profiling *)
+val get_stats: unit -> string