X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicUnivUtils.mli;h=eb55a47eb689e679128f930a48538faf291bb8d9;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=2af21f8c990974ca16f9380e647d4d0cf5df0482;hpb=3530497aed9b6ef2cd057cf7fc89ceae1d524fc1;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index 2af21f8c9..eb55a47eb 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -23,14 +23,10 @@
  * 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_graph * CicUniv.universe list * Cic.obj