* http://cs.unibo.it/helm/.
*)
-(* traverses recursively a type and lists the referenced universes *)
+(** traverses recursively a type and lists the referenced universes
+ * skipping uri (that should be the object we are working on and
+ * that can't be in the environment since we are in a Qed-like state)
+ *)
val universes_of_obj:
- Cic.obj -> CicUniv.universe list
+ UriManager.uri -> Cic.obj -> CicUniv.universe list
+
(** cleans the universe graph for a given object and fills universes with URI.
* to be used on qed