let xxx_type_of_aux' m c t =
try
- Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
+ Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph))
with
| CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
;;
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked constant")
in
match cobj with
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
- | CicEnvironment.UncheckedObj (C.Variable _) ->
+ | CicEnvironment.UncheckedObj (C.Variable _,_) ->
raise (NotWellTyped "Reference to an unchecked variable")
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
;;
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked inductive type")
in
match cobj with
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked constructor")
in
match cobj with
let (cl,parsno) =
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
match obj with
let uris_and_types =
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
let params = CicUtil.params_of_obj obj in
(function uri ->
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
match obj with