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
(**********************************************
TASSI: should fail when universes will be ON
***********************************************)
- (Some CicUniv.empty_ugraph,None)
+ (** (Some CicUniv.empty_ugraph,None) *)
+ (None,None)
in
cleanup();
obj,ugraph