From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 29 Apr 2005 08:07:53 +0000 (+0000)
Subject: uses CicUniv new assertions
X-Git-Tag: single_binding~140
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c23828f150c4ad352b383370201145a44e69f74;p=helm.git

uses CicUniv new assertions
---

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 42f0b3880..09b8ae88a 100644
--- 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