let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
let b,_ = (*TASSI : FIXME*)
- are_convertible context t1'' t1 CicUniv.empty_ugraph in
+ are_convertible context t1'' t1 CicUniv.oblivion_ugraph in
if not b then begin
warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
let newstatus =
let status' =
let context = context_of_status status in
let b,_ = (* TASSI:FIXME *)
- are_convertible context t2'' t2 CicUniv.empty_ugraph
+ are_convertible context t2'' t2
+ CicUniv.oblivion_ugraph
in
if not b then begin
warn (lazy "t2'' and t2 are NOT CONVERTIBLE");