(match hd with
(Some (_, C.Decl t)) when
fst (R.are_convertible context (S.lift n t) ty
- CicUniv.empty_ugraph) -> n
+ CicUniv.oblivion_ugraph) -> n
| (Some (_, C.Def (_,ty'))) when
fst (R.are_convertible context (S.lift n ty') ty
- CicUniv.empty_ugraph) -> n
+ CicUniv.oblivion_ugraph) -> n
| _ -> find (n+1) tl
)
| [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
let uri,metasenv,_subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in