- code cleanup, especialli in Indexing where all the goal related functions have

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

diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index 27ac1680a72c8b0231f61367a68c124d3c42ab1c..fe8582e92dc21788252f83ec2c678e18db9cf409 100644 (file)
--- 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