]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUniv.ml
added the orrible hack to the parser that is needed to call CicUniv.fresh() properly
[helm.git] / helm / ocaml / cic / cicUniv.ml
index c986ae866e03ad8759126c054f3707772c245967..abb50a196482da30fee62ecdaf33e53c967c9d1a 100644 (file)
@@ -941,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