diff options
| author | herbelin | 2006-01-03 20:33:53 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-03 20:33:53 +0000 |
| commit | d8cdd16a4f9c530b3c14ea3a348fe3b94bb19600 (patch) | |
| tree | b357053e354a87b7fe5e50a34015b7173ce06646 | |
| parent | eb61ae3d531fb91506eaf1a6034758e6a6734824 (diff) | |
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
| -rw-r--r-- | lib/gmapl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |