X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=abb50a196482da30fee62ecdaf33e53c967c9d1a;hb=52fdcda3e0083391fa04a064f3e07279d975d5ba;hp=7f8266876ddbcaf891d03c8e8bc0bc8086eba685;hpb=9d3dcd6970c1e24c8191f268c441e42c8d8b6c89;p=helm.git

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 7f8266876..abb50a196 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -128,8 +128,8 @@ let are_ugraph_eq = are_ugraph_eq307
 let string_of_universe (i,u) = 
   match u with
       Some u ->
-	((string_of_int i) ^ " " ^ (UriManager.string_of_uri u))
-    | None -> (string_of_int i)
+	"(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
+    | None -> "(" ^ (string_of_int i) ^ ",None)"
 
 let string_of_universe_set l = 
   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
@@ -142,7 +142,7 @@ let string_of_node n =
   "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
 
 let string_of_arc (a,u,v) = 
-  "(" ^ (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) ^ ")"
+  (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
   
 let string_of_mal m =
   let rc = ref "" in
@@ -178,7 +178,7 @@ let partial = ref 0.0 ;;
 let reset_spent_time () = time_spent := 0.0;;
 let get_spent_time () = !time_spent ;;
 let begin_spending () =
-  assert (!partial = 0.0);
+  (*assert (!partial = 0.0);*)
   partial := Unix.gettimeofday ()
 ;;
 
@@ -419,11 +419,14 @@ exception UniverseInconsistency of string
 
 let error arc node1 closure_type node2 closure =
   let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "\tUnable to add "^ (string_of_arc arc) ^ " cause " ^ 
-   (string_of_universe node1) ^ " is in the " ^
-   closure_type ^ " closure {" ^
-   (string_of_universe_set closure) ^ "} of " ^ 
-   (string_of_universe node2) ^ "\n\n" ^
+   "   Unable to add\n" ^ 
+   "\t" ^ (string_of_arc arc) ^ "\n" ^
+   "   cause\n" ^ 
+   "\t" ^ (string_of_universe node1) ^ "\n" ^
+   "   is in the " ^ closure_type ^ " closure\n" ^
+   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+   "   of\n" ^ 
+   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
    "  ===== Universe Inconsistency detected =====\n" in
   prerr_endline s;
   raise (UniverseInconsistency s)
@@ -463,13 +466,22 @@ type universe_graph = bag
 
 let empty_ugraph = empty_bag
 
-let current_index = ref (-1)
+let current_index_anon = ref (-1)
+let current_index_named = ref (-1)
 
-let restart_numbering () = current_index := (-1) 
+let restart_numbering () = current_index_named := (-1) 
 
-let fresh () =
-  current_index := !current_index + 1;
-  (!current_index,None)
+let fresh ?uri () =
+  let i =
+    match uri with
+    | None -> 
+        current_index_anon := !current_index_anon + 1;
+        !current_index_anon
+    | Some _ -> 
+        current_index_named := !current_index_named + 1;
+        !current_index_named
+  in
+  (i,uri)
 
 let print_ugraph g = 
   prerr_endline (string_of_bag g)
@@ -929,12 +941,12 @@ let recons_graph graph =
       MAL.add (recons_univ universe) (recons_entry entry) map)
     graph MAL.empty
 
-let assert_univs_have_uri graph =
-  let assert_univ u =
+let assert_univ u =
     match u with 
     | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
     | _ -> ()
-  in
+    
+let assert_univs_have_uri graph =
   let assert_set s =
     SOF.iter (fun u -> assert_univ u) s
   in