X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicUnivUtils.mli;h=eb55a47eb689e679128f930a48538faf291bb8d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e39ac0ab59d353d2b4c2891c590671b103453ef6;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index e39ac0ab5..eb55a47eb 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -22,6 +22,11 @@
  * 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
+