diff options
| -rw-r--r-- | tactics/autorewrite.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ffadc38b44..0f1611a82b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id$ *) + open Ast open Coqast open Equality @@ -89,13 +91,12 @@ let cache_hintrewrite (_,(rbase,lrl)) = (fun (c,dummy,b,t) -> (* here we substitute the dummy value with the right one *) c,Typing.type_of (Global.env ()) Evd.empty c,b,t) lrl in - List.rev_append - (List.filter + (List.filter (fun (_,typ,_,_) -> not (List.exists (fun (_,typ',_,_) -> Term.eq_constr typ typ') oldl) - ) lrl) oldl + ) lrl) @ oldl with - | Not_found -> List.rev lrl + | Not_found -> lrl in rewtab:=Stringmap.add rbase l !rewtab |