'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.term * Cic.term * Cic.metasenv ->
'a * (Cic.term * Cic.term * Cic.metasenv)
val check_target:
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.term * Cic.term * Cic.metasenv ->
'a * (Cic.term * Cic.term * Cic.metasenv)
val check_target: