From d8cdd16a4f9c530b3c14ea3a348fe3b94bb19600 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Jan 2006 20:33:53 +0000
Subject: Modification pour que l'ordre des éléments respecte l'ordre dans
 lequel ils ont été déclarés

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7780 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/gmapl.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 17c6c4b3ea..8fc2daf96a 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -21,7 +21,7 @@ let fold = Gmap.fold
 let add x y m =
   try
     let l = Gmap.find x m in
-    Gmap.add x (if List.mem y l then l else y::l) m
+    Gmap.add x (y::list_except y l) m
   with Not_found ->
     Gmap.add x [y] m
 
-- 
cgit v1.2.3