(* $Id$ *)
+val beta_expand_time : float ref
+
module Index :
sig
module PosEqSet : Set.S
val subsumption :
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- 'a * 'b * ('c * Index.key * Index.key * 'd) * Cic.metasenv * 'e ->
- bool * Cic.substitution
+ Inference.equality ->
+ (Inference.substitution * Inference.equality) option
val superposition_left :
int ->
- Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Index.t ->
- 'a * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'c ->
- int *
- (int * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv *
- 'e list)
- list
+ Inference.equality ->
+ int * Inference.equality list
+
val superposition_right :
int ->
- Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ 'a * Cic.context * CicUniv.universe_graph ->
Index.t ->
- 'a * Inference.proof *
- (Cic.term * Index.key * Index.key * Utils.comparison) *
- Cic.metasenv * Cic.term list -> int * Inference.equality list
+ Inference.equality ->
+ int * Inference.equality list
+
val demodulation_equality :
+ ?from:string ->
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Index.t ->
Cic.term * Index.key * Cic.metasenv ->
'a * (Cic.term * Index.key * Cic.metasenv)
+val check_target:
+ Cic.context ->
+ Inference.equality -> string -> unit
+(* maxmeta for relocate *)
+val local_max : int ref