* http://cs.unibo.it/helm/.
*)
-(* traverses recursively a type and lists the referenced universes *)
-val universes_of_obj:
- Cic.obj -> CicUniv.universe list
-
(** cleans the universe graph for a given object and fills universes with URI.
* to be used on qed
*)
val clean_and_fill:
UriManager.uri -> Cic.obj -> CicUniv.universe_graph ->
- CicUniv.universe_graph
+ CicUniv.universe_graph * CicUniv.universe list