Cic.metasenv -> UriManager.uri option -> Cic.obj ->
Cic.obj * Cic.metasenv * CicUniv.universe_graph
val insert_coercions: bool ref (* initially true *)
Cic.metasenv -> UriManager.uri option -> Cic.obj ->
Cic.obj * Cic.metasenv * CicUniv.universe_graph
val insert_coercions: bool ref (* initially true *)