let cleanup_tmp = true;;
let trust_obj = function uri -> true;;
+(*let trust_obj = function uri -> false;;*)
type type_checked_obj =
CheckedObj of Cic.obj (* cooked obj *)
(* The body does not exist ==> we consider it an axiom *)
None
in
+ CicUniv.directly_to_env_begin ();
let obj = CicParser.obj_of_xml filename bodyfilename in
+ CicUniv.directly_to_env_end ();
if cleanup_tmp then
begin
Unix.unlink filename ;
ignore (Cache.find_cooked uri);true
with Not_found -> false
;;
+
+let add_type_checked_term uri obj =
+ match obj with
+ Cic.Constant (s,(Some bo),ty,ul) ->
+ Cache.add_cooked ~key:uri obj
+ | _ -> assert false
+ Cache.add_cooked
+;;