ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_proof_checking / cicUnivUtils.mli

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index 0184037a6f7ebd1791eaf847a57390cfe2a42dab..eb55a47eb689e679128f930a48538faf291bb8d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -23,18 +23,10 @@
  * http://cs.unibo.it/helm/.                                                   
  *)
 
-(** 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: 
-  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
+    CicUniv.universe_graph * CicUniv.universe list * Cic.obj