* 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 * CicUniv.universe list * Cic.obj
+