From 50c8b025a4e3ecc35c340835d6991a02f2a463c5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Nov 2004 10:02:16 +0000
Subject: 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
---
 tactics/autorewrite.ml | 9 +++++----
 1 file 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
 
-- 
cgit v1.2.3