the application context of the subterm to rewrite can not be
forgotten
match concl_pat with
| None -> None
| Some term -> Some (S.lift 1 term) in
match concl_pat with
| None -> None
| Some term -> Some (S.lift 1 term) in
- Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat
+ Some (fun c m u ->
+ let distance = pred (List.length c - List.length context) in
+ S.lift distance lifted_t1, m, u),[],lifted_concl_pat
in
let subst,metasenv',ugraph,_,selected_terms_with_context =
ProofEngineHelpers.select
in
let subst,metasenv',ugraph,_,selected_terms_with_context =
ProofEngineHelpers.select