Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Inference.equality ->
- bool * Cic.substitution
+ bool * Inference.substitution
val superposition_left :
int ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
'a * (Cic.term * Index.key * Cic.metasenv)
val check_target:
Cic.context ->
- Inference.equality -> string -> Cic.term * CicUniv.universe_graph
+ Inference.equality -> string -> unit
(* maxmeta for relocate *)
val local_max : int ref