X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicUnivUtils.mli;h=0184037a6f7ebd1791eaf847a57390cfe2a42dab;hb=58bd1746df1d9dc734f8ac75220d25997c09bed1;hp=2af21f8c990974ca16f9380e647d4d0cf5df0482;hpb=c4afa186c53998a10eab85d3fcc113b07bccfdf9;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index 2af21f8c9..0184037a6 100644
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -23,9 +23,13 @@
  * 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