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 ->
goal list
val superposition_right :
+ ?subterms_only:bool ->
int ->
'a * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.context ->
Equality.equality -> string -> unit
+ (** profiling *)
+val get_stats: unit -> string