added clean_and_fill, to be invoked on qed

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index 8182f72e3260e16c4dd76572d6893700a774c7d0..1c072bea5c434ff80826e377a2331b486a48d667 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -150,8 +150,8 @@ let universes_of_obj t =
                  fun y (_,t) -> y @ aux t) 
                [] l') 
              [] l) @ 
-          (List.fold_left (
-             fun l u -> 
+          (List.fold_left
+              (fun l u -> 
               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
                              CicUniv.empty_ugraph))
              [] v)
@@ -159,5 +159,9 @@ let universes_of_obj t =
   in 
     aux_obj (t,CicUniv.empty_ugraph) 
 
-
+let clean_and_fill uri obj ugraph =
+  let list_of_universes = universes_of_obj obj in
+  let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
+  let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
+  ugraph
 

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
index e39ac0ab59d353d2b4c2891c590671b103453ef6..2af21f8c990974ca16f9380e647d4d0cf5df0482 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.mli
@@ -22,6 +22,15 @@
  * 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
+