match entry with
t when t == hyp_to_clear_body ->
let cleared_entry =
- let ty =
+ let ty,_ =
CicTypeChecker.type_of_aux' metasenv context term
+ CicUniv.empty_ugraph (* TASSI: FIXME *)
in
Some (n_to_clear_body, Cic.Decl ty)
in
| None -> None::context
| Some (n,C.Decl t)
| Some (n,C.Def (t,None)) ->
- let _ =
+ let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.empty_ugraph (* TASSI: FIXME *)
with
_ ->
raise
| Some (_,Cic.Def (_,Some _)) -> assert false
) canonical_context []
in
- let _ =
+ let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+ CicUniv.empty_ugraph (* TASSI: FIXME *)
with
_ ->
raise
| Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
| Some (n,C.Def (t,None)) ->
- let _ =
+ let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.empty_ugraph (* TASSI: FIXME *)
with
_ ->
raise
entry::context
) canonical_context []
in
- let _ =
+ let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+ CicUniv.empty_ugraph (* TASSI: FIXME *)
with
_ ->
raise