uses CicUniv new assertions

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 42f0b3880e676e4bcdfac8e200c912dd978ddeb5..09b8ae88ac9935e4db18f9eb4b25e6ede7cb37b7 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -393,6 +393,7 @@ module Cache :
            None -> 
              assert false (* only NON dummy universes can be committed *)
          | Some g ->
+              CicUniv.assert_univs_have_uri g;
              frozen_list := List.remove_assq uri !frozen_list ;
              HT.add cacheOfCookedObjects uri (obj,g) 
     with
@@ -537,7 +538,8 @@ let get_object_to_add uri =
      (**********************************************
        TASSI: should fail when universes will be ON
      ***********************************************)
-     (Some CicUniv.empty_ugraph,None)
+     (** (Some CicUniv.empty_ugraph,None) *)
+     (None,None)
  in
    cleanup();
    obj,ugraph