let rec scan_tac ~old_context_length ~index ~tactic =
let scan_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let context_length = List.length context in
let rec aux index =
let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
let elim_clear_unfold_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = PEH.lookup_type metasenv context what in
let tac =
?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in
- let _, metasenv,_,_, _ = proof in
+ let _, metasenv, _subst, _,_, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in