let lifted_gty = CicSubstitution.lift 1 gty in
let lifted_conjecture =
metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
- let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in
+ let lifted_pattern =
+ Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat
+ in
let subst,metasenv',ugraph,_,selected_terms_with_context =
ProofEngineHelpers.select
~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let with_what, metasenv, u = with_what context metasenv u in
let with_what = CicMetaSubst.apply_subst subst with_what in
let pbo = CicMetaSubst.apply_subst subst pbo in
let pty = CicMetaSubst.apply_subst subst pty in