* For details, see the HELM World-Wide-Web page,
* 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
+