module TC = CicTypeChecker
module LO = LibraryObjects
module DTI = DoubleTypeInference
+module HEL = HExtlib
let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
Some (rewrite (None, [(s, hole)], None))
| _ -> None
in
- let rew_hips = PEH.list_rev_map_filter (map hyp) context in
+ let rew_hips = HEL.list_rev_map_filter (map hyp) context in
let rew_concl = rewrite (None, [], Some hole) in
let clear = PESR.clear ~hyps:[hyp; var] in
let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
let (proof, goal) = status in
let (_, metasenv, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let tactics = PEH.list_rev_map_filter map context in
+ let tactics = HEL.list_rev_map_filter map context in
PET.apply_tactic (T.seq ~tactics) status
in
PET.mk_tactic subst_tac