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"
| 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 =