diff options
| author | herbelin | 2004-11-22 10:02:16 +0000 |
|---|---|---|
| committer | herbelin | 2004-11-22 10:02:16 +0000 |
| commit | 50c8b025a4e3ecc35c340835d6991a02f2a463c5 (patch) | |
| tree | de5afd37bd032c476bd4cd557ff89461715dbfee | |
| parent | a215993ad9e073fc09825742494ec06a9f8d6c84 (diff) | |
Réparation incompatibilité de comportement introduite lors de mise en compatibilité avec Write State
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6339 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |