with type elt = Utils.pos * Equality.equality
and type t = Equality_indexing.DT.PosEqSet.t
type t =
- Discrimination_tree.DiscriminationTreeIndexing(Discrimination_tree.CicIndexable)(PosEqSet).t
+ Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
end
+val check_for_duplicates : Cic.metasenv -> string -> unit
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
Equality.equality ->
int * Equality.equality list
+val demod :
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal ->
+ bool * Equality.goal
val demodulation_equality :
Equality.equality_bag ->
?from:string ->