module FNG = FreshNamesGenerator
module MI = CicMkImplicit
module PESR = ProofEngineStructuralRules
+module HEL = HExtlib
let fail_msg0 = "unexported clearbody: invalid argument"
let fail_msg2 = "fwd: no applicable simplification"
let id_tac =
let id_tac (proof,goal) =
try
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
with CicUtil.Meta_not_found _ -> (proof, [])
in
let clearbody status =
let (proof, goal) = status in
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
in
| Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
| _ -> None
in
- PEH.list_rev_map_filter aux terms
+ HEL.list_rev_map_filter aux terms
let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
- let xuri, metasenv, u, t = proof in
+ let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
T.then_ ~start:(letin_tac conclusion)
~continuation:(clearbody ~index:1)
in
- let proof = (xuri, metasenv, u, t) in
+ let proof = (xuri, metasenv, _subst, u, t, attrs) in
let aux (proof, goals) (tac, goal) =
let proof, new_goals = PET.apply_tactic tac (proof, goal) in
proof, goals @ new_goals
(* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
let lapply_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 lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
let tac =
in
let fwd_simpl_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, ty = CicUtil.lookup_meta goal metasenv in
let index, major = PEH.lookup_type metasenv context hyp in
match FwdQueries.fwd_simpl ~dbd major with