let lapply_tac (proof, goal) =
let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+ let lemma, _ = TC.type_of_aux' metasenv context what U.oblivion_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
let conclusion =