with type elt = Utils.pos * Equality.equality
and type t = Equality_indexing.DT.PosEqSet.t
type t =
- Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t
+ Discrimination_tree.Make(Cic_indexable.CicIndexable)(PosEqSet).t
end
val check_for_duplicates : Cic.metasenv -> string -> unit
Index.t ->
Equality.goal ->
bool * Equality.goal
+val demodulation_all_goal :
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal -> int ->
+ Equality.goal list
val demodulation_theorem :
Equality.equality_bag ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.goal ->
int ->
- Equality.goal option
-
+ (Equality.equality_bag * Equality.goal_proof * Cic.metasenv *
+ Subst.substitution * Equality.proof) option
- (** profiling *)
-val get_stats: unit -> string