let map (_context_of_t, t) l = t :: l in
let what = List.fold_right map selected_terms [] in
let arg' = MS.apply_subst subst arg' in
- let argty = MS.apply_subst subst argty in
let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
let pred = MS.apply_subst subst pred in
- let pred = C.Lambda (fresh_name, argty, pred) in
+ let pred = C.Lambda (fresh_name, C.Implicit None, pred) in
let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
mk_pred metasenv subst (hyp :: context') pred arg' cpattern' tail
in
let metasenv, subst, pred, arg =
mk_pred metasenv subst context goal arg cpattern (List.rev actual_args)
in
+ HLog.debug ("PREDICATE CONTEXT:\n" ^ CicPp.ppcontext ~metasenv context);
HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
metasenv, subst, pred, arg, actual_args
let refined_term,_refined_termty,metasenv'',subst,_ugraph =
CicRefine.type_of metasenv' subst context term_to_refine ugraph
in
+ let ipred = match refined_term with
+ | C.Appl ts -> List.nth ts (List.length ts - pred_pos)
+ | _ -> assert false
+ in
let new_goals =
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
let res = proof'', patched_new_goals in
let upto = List.length actual_args in
- if upto = 0 then res else
- let continuation = beta_after_elim_tac upto pred in
+ if upto = 0 then res else
+(* FG: we use ipred (instantiated pred) instead of pred (not instantiated) *)
+ let continuation = beta_after_elim_tac upto ipred in
let dummy_status = proof,goal in
PET.apply_tactic
(T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)