Index.t ->
Equality.equality ->
(Subst.substitution * Equality.equality * bool) option
-
+val unification_all :
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.equality ->
+ (Subst.substitution * Equality.equality * bool) list
+val subsumption_all :
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.equality ->
+ (Subst.substitution * Equality.equality * bool) list
val superposition_left :
Equality.equality_bag ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Equality.equality_bag ->
Cic.context ->
Equality.equality -> string -> unit
+val solve_demodulating:
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal ->
+ int ->
+ Equality.goal option
+
(** profiling *)
val get_stats: unit -> string