From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 11 Jan 2005 16:03:13 +0000 (+0000)
Subject: added clean_and_fill, to be invoked on qed
X-Git-Tag: V_0_1_0~148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3530497aed9b6ef2cd057cf7fc89ceae1d524fc1;p=helm.git

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 8182f72e3..1c072bea5 100644
--- 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 e39ac0ab5..2af21f8c9 100644
--- 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
+