packaging cleanup: get rid of ancient debhelpers, use dh_install

[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 e39ac0ab59d353d2b4c2891c590671b103453ef6..0184037a6f7ebd1791eaf847a57390cfe2a42dab 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -22,6 +22,19 @@
  * 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
+