* For details, see the HELM World-Wide-Web page,
* 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
+ *)
+val clean_and_fill:
+ UriManager.uri -> Cic.obj -> CicUniv.universe_graph ->
+ CicUniv.universe_graph
+