X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FfwdSimplTactic.ml;h=fa7d4aef1543997e69609071e89e7c379b199860;hb=d669da59d27e2418e65a275dc5d405237db2b93a;hp=ffc90c1cc4948f44c99ee3a1852d20fbaa93aca5;hpb=e31bb143e3a303321e509f415764338849b7e516;p=helm.git

diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml
index ffc90c1cc..fa7d4aef1 100644
--- a/helm/software/components/tactics/fwdSimplTactic.ml
+++ b/helm/software/components/tactics/fwdSimplTactic.ml
@@ -35,6 +35,7 @@ module T = Tacticals
 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"
@@ -102,7 +103,7 @@ let get_clearables context terms =
       | 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 =