-(* set_type_checking_info uri *)
-(* must be called once the type-checking of uri is finished *)
-(* The object whose uri is uri is unfreezed *)
-let set_type_checking_info uri =
- Cache.frozen_to_cooked uri
- (fun ~object_to_cook:obj ~add_cooked ->
- (* let's cook the object at every level *)
- let obj' = CicSubstitution.undebrujin_inductive_def uri obj in
- add_cooked (uri,0) obj' ;
- let cooked_objs = !cook_obj obj' uri in
- let last_cooked_level = ref 0 in
- let last_cooked_obj = ref obj' in
- List.iter
- (fun (n,cobj) ->
- for i = !last_cooked_level + 1 to n do
- add_cooked (uri,i) !last_cooked_obj
- done ;
- add_cooked (uri,n + 1) cobj ;
- last_cooked_level := n + 1 ;
- last_cooked_obj := cobj
- ) cooked_objs ;
- for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do
- add_cooked (uri,i) !last_cooked_obj
- done
- )
+(* get_cooked_obj uri *)
+(* returns the cooked cic object whose uri is uri. The term must be present *)
+(* and cooked in cache *)
+let get_cooked_obj uri =
+ try
+ Cache.find_cooked uri
+ with Not_found ->
+ if not (!trust_obj uri) then
+ prerr_endline ("@@@ OOOOOOOPS: WE TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE SHOULD NOT DO THAT! THAT MEANS LOOKING FOR TROUBLES ;-(") ;
+ match is_type_checked uri with
+ CheckedObj obj -> obj
+ | _ -> assert false