let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
(try
ignore
(CicTypeChecker.type_of_aux' metasenv context te
- CicUniv.empty_ugraph (* TASSI: FIXME *));
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
ignore
(CicTypeChecker.type_of_aux' metasenv context ty
- CicUniv.empty_ugraph (* TASSI: FIXME *));
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
with
_ ->
raise
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise
(PET.Fail
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in