renommage NoRedun vers le plus joli NoDup

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 159 insertions, 157 deletions

diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
index 22ff07c1ff..078d58d500 100644
--- a/theories/FSets/FMapWeakInterface.v
+++ b/theories/FSets/FMapWeakInterface.v
@@ -150,7 +150,7 @@ Module Type S.
         MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
       Parameter elements_2 : 
         InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
-      Parameter elements_3 : noredunA eq_key (elements m).  
+      Parameter elements_3 : NoDupA eq_key (elements m).  
 
     (** Specification of [fold] *)  
       Parameter fold_1 :
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 6c544053e9..89699f3f9e 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -44,7 +44,7 @@ Notation eqk := (eqk (elt:=elt)).
 Notation eqke := (eqke (elt:=elt)).
 Notation MapsTo := (MapsTo (elt:=elt)).
 Notation In := (In (elt:=elt)).
-Notation noredunA := (noredunA eqk).
+Notation NoDupA := (NoDupA eqk).
 
 (** * [empty] *)
 
@@ -62,7 +62,7 @@ Qed.
 
 Hint Resolve empty_1.
 
-Lemma empty_noredun : noredunA empty.
+Lemma empty_NoDup : NoDupA empty.
 Proof. 
  unfold empty; auto.
 Qed.
@@ -97,12 +97,12 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
    | (k',_) :: l => if X.eq_dec k k' then true else mem k l
   end.
 
-Lemma mem_1 : forall m (Hm:noredunA m) x, In x m -> mem x m = true.
+Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.
 Proof.
  intros m Hm x; generalize Hm; clear Hm.      
- functional induction mem x m;intros noredun belong1;trivial.
+ functional induction mem x m;intros NoDup belong1;trivial.
  inversion belong1. inversion H.
- inversion_clear noredun.
+ inversion_clear NoDup.
  inversion_clear belong1.
  inversion_clear H3.
  compute in H4; destruct H4.
@@ -111,12 +111,12 @@ Proof.
  exists x; auto.
 Qed. 
 
-Lemma mem_2 : forall m (Hm:noredunA m) x, mem x m = true -> In x m. 
+Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m. 
 Proof.
  intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo.
- functional induction mem x m; intros noredun hyp; try discriminate.
+ functional induction mem x m; intros NoDup hyp; try discriminate.
  exists e; auto. 
- inversion_clear noredun.
+ inversion_clear NoDup.
  destruct H0; auto.
  exists x; auto.
 Qed.
@@ -135,7 +135,7 @@ Proof.
  functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto.
 Qed.
 
-Lemma find_1 : forall m (Hm:noredunA m) x e, 
+Lemma find_1 : forall m (Hm:NoDupA m) x e, 
   MapsTo x e m -> find x m = Some e. 
 Proof.
  intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo.
@@ -153,7 +153,7 @@ Qed.
 
 (* Not part of the exported specifications, used later for [combine]. *)
 
-Lemma find_eq : forall m (Hm:noredunA m) x x', 
+Lemma find_eq : forall m (Hm:NoDupA m) x x', 
    X.eq x x' -> find x m = find x' m.
 Proof.
  induction m; simpl; auto; destruct a; intros.
@@ -213,7 +213,7 @@ Proof.
  inversion_clear 2; auto.
 Qed.
 
-Lemma add_noredun : forall m (Hm:noredunA m) x e, noredunA (add x e m).
+Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m).
 Proof.
  induction m.
  simpl; constructor; auto; red; inversion 1.
@@ -229,22 +229,22 @@ Qed.
 
 (* Not part of the exported specifications, used later for [combine]. *)
 
-Lemma add_eq : forall m (Hm:noredunA m) x a e, 
+Lemma add_eq : forall m (Hm:NoDupA m) x a e, 
    X.eq x a -> find x (add a e m) = Some e.
 Proof.
  intros.
  apply find_1; auto.
- apply add_noredun; auto.
+ apply add_NoDup; auto.
  apply add_1; auto.
 Qed.
 
-Lemma add_not_eq : forall m (Hm:noredunA m) x a e, 
+Lemma add_not_eq : forall m (Hm:NoDupA m) x a e, 
   ~X.eq x a -> find x (add a e m) = find x m.
 Proof.
  intros.
  case_eq (find x m); intros.
  apply find_1; auto.
- apply add_noredun; auto.
+ apply add_NoDup; auto.
  apply add_2; auto.
  apply find_2; auto.
  case_eq (find x (add a e m)); intros; auto.
@@ -263,7 +263,7 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
    | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l
   end.  
 
-Lemma remove_1 : forall m (Hm:noredunA m) x y, X.eq x y -> ~ In y (remove x m).
+Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m).
 Proof.
  intros m Hm x y; generalize Hm; clear Hm.
  functional induction remove x m;simpl;intros;auto.
@@ -286,7 +286,7 @@ Proof.
  exists e; auto.
 Qed.
   
-Lemma remove_2 : forall m (Hm:noredunA m) x y e, 
+Lemma remove_2 : forall m (Hm:NoDupA m) x y e, 
   ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
@@ -298,7 +298,7 @@ Proof.
  inversion_clear 1; inversion_clear 2; auto.
 Qed.
 
-Lemma remove_3 : forall m (Hm:noredunA m) x y e, 
+Lemma remove_3 : forall m (Hm:NoDupA m) x y e, 
   MapsTo y e (remove x m) -> MapsTo y e m.
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
@@ -306,7 +306,7 @@ Proof.
  do 2 inversion_clear 1; auto.
 Qed.
 
-Lemma remove_3' : forall m (Hm:noredunA m) x y e, 
+Lemma remove_3' : forall m (Hm:NoDupA m) x y e, 
   InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
@@ -314,7 +314,7 @@ Proof.
  do 2 inversion_clear 1; auto.
 Qed.
 
-Lemma remove_noredun : forall m (Hm:noredunA m) x, noredunA (remove x m).
+Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m).
 Proof.
  induction m.
  simpl; intuition.
@@ -340,7 +340,7 @@ Proof.
 auto.
 Qed.
 
-Lemma elements_3 : forall m (Hm:noredunA m), noredunA (elements m). 
+Lemma elements_3 : forall m (Hm:NoDupA m), NoDupA (elements m). 
 Proof. 
  auto.
 Qed.
@@ -382,7 +382,7 @@ Definition Equal cmp m m' :=
   (forall k, In k m <-> In k m') /\ 
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
-Lemma submap_1 : forall m (Hm:noredunA m) m' (Hm': noredunA m') cmp, 
+Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, 
   Submap cmp m m' -> submap cmp m m' = true. 
 Proof.
  unfold Submap, submap.
@@ -403,7 +403,7 @@ Proof.
  apply H0 with k; auto.
 Qed.
    
-Lemma submap_2 : forall m (Hm:noredunA m) m' (Hm': noredunA m') cmp, 
+Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, 
   submap cmp m m' = true -> Submap cmp m m'. 
 Proof.
  unfold Submap, submap.
@@ -444,7 +444,7 @@ Qed.
 
 (** Specification of [equal] *)
 
-Lemma equal_1 : forall m (Hm:noredunA m) m' (Hm': noredunA m') cmp, 
+Lemma equal_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, 
   Equal cmp m m' -> equal cmp m m' = true. 
 Proof. 
  unfold Equal, equal.
@@ -452,7 +452,7 @@ Proof.
  apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder.
 Qed.
 
-Lemma equal_2 : forall m (Hm:noredunA m) m' (Hm':noredunA m') cmp, 
+Lemma equal_2 : forall m (Hm:NoDupA m) m' (Hm':NoDupA m') cmp, 
   equal cmp m m' = true -> Equal cmp m m'.
 Proof.
  unfold Equal, equal.
@@ -526,8 +526,8 @@ Proof.
  constructor 2; auto.
 Qed.
 
-Lemma map_noredun : forall m (Hm : noredunA (@eqk elt) m)(f:elt->elt'), 
-  noredunA (@eqk elt') (map f m).
+Lemma map_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f:elt->elt'), 
+  NoDupA (@eqk elt') (map f m).
 Proof.   
  induction m; simpl; auto.
  intros.
@@ -586,8 +586,8 @@ Proof.
  constructor 2; auto.
 Qed.
 
-Lemma mapi_noredun : forall m (Hm : noredunA (@eqk elt) m)(f: key->elt->elt'), 
-  noredunA (@eqk elt') (mapi f m).
+Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'), 
+  NoDupA (@eqk elt') (mapi f m).
 Proof.
  induction m; simpl; auto.
  intros.
@@ -622,28 +622,28 @@ Definition combine (m:t elt)(m':t elt') : t oee' :=
   let r := combine_r m m' in 
   fold_right_pair (add (elt:=oee')) l r.
 
-Lemma fold_right_pair_noredun : 
-  forall l r (Hl: noredunA (eqk (elt:=oee')) l) 
-    (Hl: noredunA (eqk (elt:=oee')) r), 
-    noredunA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r).
+Lemma fold_right_pair_NoDup : 
+  forall l r (Hl: NoDupA (eqk (elt:=oee')) l) 
+    (Hl: NoDupA (eqk (elt:=oee')) r), 
+    NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r).
 Proof.
  induction l; simpl; auto.
  destruct a; simpl; auto.
  inversion_clear 1.
- intros; apply add_noredun; auto.
+ intros; apply add_NoDup; auto.
 Qed.
-Hint Resolve fold_right_pair_noredun.
+Hint Resolve fold_right_pair_NoDup.
 
-Lemma combine_noredun : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m'), 
-  noredunA (@eqk oee') (combine m m').
+Lemma combine_NoDup : 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), 
+  NoDupA (@eqk oee') (combine m m').
 Proof.
  unfold combine, combine_r, combine_l.
  intros.
  set (f1 := fun (k : key) (e : elt) => (Some e, find k m')).
  set (f2 := fun (k : key) (e' : elt') => (find k m, Some e')).
- generalize (mapi_noredun Hm f1).
- generalize (mapi_noredun Hm' f2).
+ generalize (mapi_NoDup Hm f1).
+ generalize (mapi_NoDup Hm' f2).
  set (l := mapi f1 m); clearbody l.
  set (r := mapi f2 m'); clearbody r.
  auto.
@@ -662,7 +662,7 @@ Definition at_least_right (o:option elt)(o':option elt') :=
   end.
 
 Lemma combine_l_1 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key), 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), 
   find x (combine_l m m') = at_least_left (find x m) (find x m'). 
 Proof.
  unfold combine_l.
@@ -670,7 +670,7 @@ Proof.
  case_eq (find x m); intros.
  simpl.
  apply find_1.
- apply mapi_noredun; auto.
+ apply mapi_NoDup; auto.
  destruct (mapi_1 (fun k e => (Some e, find k m')) (find_2 H)) as (y,(H0,H1)).
  rewrite (find_eq Hm' (X.eq_sym H0)); auto.
  simpl.
@@ -681,7 +681,7 @@ Proof.
 Qed.
 
 Lemma combine_r_1 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key), 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), 
   find x (combine_r m m') = at_least_right (find x m) (find x m'). 
 Proof.
  unfold combine_r.
@@ -689,7 +689,7 @@ Proof.
  case_eq (find x m'); intros.
  simpl.
  apply find_1.
- apply mapi_noredun; auto.
+ apply mapi_NoDup; auto.
  destruct (mapi_1 (fun k e => (find k m, Some e)) (find_2 H)) as (y,(H0,H1)).
  rewrite (find_eq Hm (X.eq_sym H0)); auto.
  simpl.
@@ -706,17 +706,17 @@ Definition at_least_one (o:option elt)(o':option elt') :=
   end.
 
 Lemma combine_1 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key), 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), 
   find x (combine m m') = at_least_one (find x m) (find x m'). 
 Proof.
  unfold combine.
  intros.
  generalize (combine_r_1 Hm Hm' x).
  generalize (combine_l_1 Hm Hm' x).
- assert (noredunA (eqk (elt:=oee')) (combine_l m m')).
-  unfold combine_l; apply mapi_noredun; auto.
- assert (noredunA (eqk (elt:=oee')) (combine_r m m')).
-  unfold combine_r; apply mapi_noredun; auto.
+ assert (NoDupA (eqk (elt:=oee')) (combine_l m m')).
+  unfold combine_l; apply mapi_NoDup; auto.
+ assert (NoDupA (eqk (elt:=oee')) (combine_r m m')).
+  unfold combine_r; apply mapi_NoDup; auto.
  set (l := combine_l m m') in *; clearbody l.
  set (r := combine_r m m') in *; clearbody r.
  set (o := find x m); clearbody o.
@@ -749,16 +749,16 @@ Definition map2 m m' :=
   let m1 : t (option elt'') := map (fun p => f (fst p) (snd p)) m0 in 
   fold_right_pair (option_cons (A:=elt'')) m1 nil.
 
-Lemma map2_noredun : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m'), 
-  noredunA (@eqk elt'') (map2 m m').
+Lemma map2_NoDup : 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), 
+  NoDupA (@eqk elt'') (map2 m m').
 Proof.
  intros.
  unfold map2.
- assert (H0:=combine_noredun Hm Hm').
+ assert (H0:=combine_NoDup Hm Hm').
  set (l0:=combine m m') in *; clearbody l0.
  set (f':= fun p : oee' => f (fst p) (snd p)).
- assert (H1:=map_noredun (elt' := option elt'') H0 f').
+ assert (H1:=map_NoDup (elt' := option elt'') H0 f').
  set (l1:=map f' l0) in *; clearbody l1. 
  clear f' f H0 l0 Hm Hm' m m'.
  induction l1.
@@ -782,13 +782,13 @@ Definition at_least_one_then_f (o:option elt)(o':option elt') :=
   end.
 
 Lemma map2_0 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key), 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), 
   find x (map2 m m') = at_least_one_then_f (find x m) (find x m'). 
 Proof.
  intros.
  unfold map2.
  assert (H:=combine_1 Hm Hm' x).
- assert (H2:=combine_noredun Hm Hm').
+ assert (H2:=combine_NoDup Hm Hm').
  set (f':= fun p : oee' => f (fst p) (snd p)).
  set (m0 := combine m m') in *; clearbody m0.
  set (o:=find x m) in *; clearbody o. 
@@ -839,7 +839,7 @@ Qed.
 
 (** Specification of [map2] *)
 Lemma map2_1 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key),
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key),
   In x m \/ In x m' -> 
   find x (map2 m m') = f (find x m) (find x m'). 
 Proof.
@@ -853,13 +853,13 @@ Proof.
 Qed.
  
 Lemma map2_2 : 
-  forall m (Hm:noredunA (@eqk elt) m) m' (Hm':noredunA (@eqk elt') m')(x:key), 
+  forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), 
   In x (map2 m m') -> In x m \/ In x m'. 
 Proof.
  intros.
  destruct H as (e,H).
  generalize (map2_0 Hm Hm' x).
- rewrite (find_1 (map2_noredun Hm Hm') H).
+ rewrite (find_1 (map2_NoDup Hm Hm') H).
  generalize (@find_2 _ m x).
  generalize (@find_2 _ m' x).
  destruct (find x m); 
@@ -881,7 +881,7 @@ Module Make (X: DecidableType) <: S with Module E:=X.
  Definition key := X.t. 
 
  Record slist (elt:Set) : Set :=  
-  {this :> Raw.t elt; noredun : noredunA (@Raw.PX.eqk elt) this}.
+  {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}.
  Definition t (elt:Set) := slist elt. 
 
  Section Elt. 
@@ -889,16 +889,16 @@ Module Make (X: DecidableType) <: S with Module E:=X.
 
  Implicit Types m : t elt.
 
- Definition empty := Build_slist (Raw.empty_noredun elt).
+ Definition empty := Build_slist (Raw.empty_NoDup elt).
  Definition is_empty m := Raw.is_empty m.(this).
- Definition add x e m := Build_slist (Raw.add_noredun m.(noredun) x e).
+ Definition add x e m := Build_slist (Raw.add_NoDup m.(NoDup) x e).
  Definition find x m := Raw.find x m.(this).
- Definition remove x m := Build_slist (Raw.remove_noredun m.(noredun) x). 
+ Definition remove x m := Build_slist (Raw.remove_NoDup m.(NoDup) x). 
  Definition mem x m := Raw.mem x m.(this).
- Definition map f m : t elt' := Build_slist (Raw.map_noredun m.(noredun) f).
- Definition mapi f m : t elt' := Build_slist (Raw.mapi_noredun m.(noredun) f).
+ Definition map f m : t elt' := Build_slist (Raw.map_NoDup m.(NoDup) f).
+ Definition mapi f m : t elt' := Build_slist (Raw.mapi_NoDup m.(NoDup) f).
  Definition map2 f m (m':t elt') : t elt'' := 
- Build_slist (Raw.map2_noredun f m.(noredun) m'.(noredun)).
+ Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)).
  Definition elements m := @Raw.elements elt m.(this).
  Definition fold A f m i := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' := @Raw.equal elt cmp m.(this) m'.(this).
@@ -915,8 +915,8 @@ Module Make (X: DecidableType) <: S with Module E:=X.
 
  Definition MapsTo_1 m := @Raw.PX.MapsTo_eq elt m.(this).
 
- Definition mem_1 m := @Raw.mem_1 elt m.(this) m.(noredun).
- Definition mem_2 m := @Raw.mem_2 elt m.(this) m.(noredun).
+ Definition mem_1 m := @Raw.mem_1 elt m.(this) m.(NoDup).
+ Definition mem_2 m := @Raw.mem_2 elt m.(this) m.(NoDup).
 
  Definition empty_1 := @Raw.empty_1.
 
@@ -927,16 +927,16 @@ Module Make (X: DecidableType) <: S with Module E:=X.
  Definition add_2 m := @Raw.add_2 elt m.(this).
  Definition add_3 m := @Raw.add_3 elt m.(this).
 
- Definition remove_1 m := @Raw.remove_1 elt m.(this) m.(noredun).
- Definition remove_2 m := @Raw.remove_2 elt m.(this) m.(noredun).
- Definition remove_3 m := @Raw.remove_3 elt m.(this) m.(noredun).
+ Definition remove_1 m := @Raw.remove_1 elt m.(this) m.(NoDup).
+ Definition remove_2 m := @Raw.remove_2 elt m.(this) m.(NoDup).
+ Definition remove_3 m := @Raw.remove_3 elt m.(this) m.(NoDup).
 
- Definition find_1 m := @Raw.find_1 elt m.(this) m.(noredun).
+ Definition find_1 m := @Raw.find_1 elt m.(this) m.(NoDup).
  Definition find_2 m := @Raw.find_2 elt m.(this).
 
  Definition elements_1 m := @Raw.elements_1 elt m.(this).
  Definition elements_2 m := @Raw.elements_2 elt m.(this).
- Definition elements_3 m := @Raw.elements_3 elt m.(this) m.(noredun).
+ Definition elements_3 m := @Raw.elements_3 elt m.(this) m.(NoDup).
 
  Definition fold_1 m := @Raw.fold_1 elt m.(this).
 
@@ -947,12 +947,12 @@ Module Make (X: DecidableType) <: S with Module E:=X.
  Definition mapi_2 m := @Raw.mapi_2 elt elt' m.(this).
 
  Definition map2_1 m (m':t elt') x f := 
-  @Raw.map2_1 elt elt' elt'' f m.(this) m.(noredun) m'.(this) m'.(noredun) x.
+  @Raw.map2_1 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x.
  Definition map2_2 m (m':t elt') x f := 
-  @Raw.map2_2 elt elt' elt'' f m.(this) m.(noredun) m'.(this) m'.(noredun) x.
+  @Raw.map2_2 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x.
 
- Definition equal_1 m m' := @Raw.equal_1 elt m.(this) m.(noredun) m'.(this) m'.(noredun).
- Definition equal_2 m m' := @Raw.equal_2 elt m.(this) m.(noredun) m'.(this) m'.(noredun).
+ Definition equal_1 m m' := @Raw.equal_1 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup).
+ Definition equal_2 m m' := @Raw.equal_2 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup).
 
  End Elt.
 End Make.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index b67c1245e2..66d019d6f1 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -449,15 +449,15 @@ Module Properties (M: S).
     remove_diff_singleton diff_inter_empty diff_inter_all Add_add Add_remove
     Equal_remove : set.
 
-  Notation NoRedun := (noredunA E.eq).
+  Notation NoDup := (NoDupA E.eq).
 
-  Section noredunA_Remove.
+  Section NoDupA_Remove.
 
   Definition remove_list x l := MoreList.filter (fun y => negb (eqb x y)) l.
 
   Lemma remove_list_correct :
-    forall s x, NoRedun s -> 
-    NoRedun (remove_list x s) /\
+    forall s x, NoDup s -> 
+    NoDup (remove_list x s) /\
     (forall y : elt, ME.In y (remove_list x s) <-> ME.In y s /\ ~ E.eq x y).
   Proof.
    simple induction s; simpl; intros.
@@ -486,7 +486,7 @@ Module Properties (M: S).
   Let ListEq l l' := forall y : elt, ME.In y l <-> ME.In y l'.
 
   Lemma remove_list_equal :
-    forall s s' x, NoRedun (x :: s) -> NoRedun s' -> 
+    forall s s' x, NoDup (x :: s) -> NoDup s' -> 
     ListEq (x :: s) s' -> ListEq s (remove_list x s').
   Proof.  
    unfold ListEq; intros. 
@@ -505,7 +505,7 @@ Module Properties (M: S).
   Let ListAdd x l l' := forall y : elt, ME.In y l' <-> E.eq x y \/ ME.In y l.
 
   Lemma remove_list_add :
-    forall s s' x x', NoRedun s -> NoRedun (x' :: s') ->
+    forall s s' x x', NoDup s -> NoDup (x' :: s') ->
     ~ E.eq x x' -> ~ ME.In x s -> 
     ListAdd x s (x' :: s') -> ListAdd x (remove_list x' s) s'.
   Proof.
@@ -534,7 +534,7 @@ Module Properties (M: S).
   Variables (i:A).
 
   Lemma remove_list_fold_right_0 :
-    forall s x, NoRedun s -> ~ME.In x s ->
+    forall s x, NoDup s -> ~ME.In x s ->
     eqA (fold_right f i s) (fold_right f i (remove_list x s)).
   Proof.
    simple induction s; simpl; intros.
@@ -546,7 +546,7 @@ Module Properties (M: S).
   Qed.   
 
   Lemma remove_list_fold_right :
-    forall s x, NoRedun s -> ME.In x s ->
+    forall s x, NoDup s -> ME.In x s ->
     eqA (fold_right f i s) (f x (fold_right f i (remove_list x s))).
   Proof.
    simple induction s; simpl.  
@@ -563,7 +563,7 @@ Module Properties (M: S).
   Qed.   
 
   Lemma fold_right_equal :
-    forall s s', NoRedun s -> NoRedun s' ->
+    forall s s', NoDup s -> NoDup s' ->
     ListEq s s' -> eqA (fold_right f i s) (fold_right f i s').
   Proof.
    simple induction s.
@@ -586,7 +586,7 @@ Module Properties (M: S).
   Qed.
 
   Lemma fold_right_add :
-    forall s' s x, NoRedun s -> NoRedun s' -> ~ ME.In x s ->
+    forall s' s x, NoDup s -> NoDup s' -> ~ ME.In x s ->
     ListAdd x s s' -> eqA (fold_right f i s') (f x (fold_right f i s)).
   Proof.   
    simple induction s'.
@@ -625,7 +625,7 @@ Module Properties (M: S).
    destruct H; auto; destruct n; auto.
   Qed.
 
-  End noredunA_Remove.
+  End NoDupA_Remove.
 
   (** * Alternative (weaker) specifications for [fold] *)
 
@@ -638,12 +638,12 @@ Module Properties (M: S).
   Lemma fold_0 : 
       forall s (A : Set) (i : A) (f : elt -> A -> A),
       exists l : list elt,
-        NoRedun l /\
+        NoDup l /\
         (forall x : elt, In x s <-> InA E.eq x l) /\
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply noredunA_rev; auto.
+  apply NoDupA_rev; auto.
   exact E.eq_trans.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
@@ -694,7 +694,7 @@ Module Properties (M: S).
 
   Lemma cardinal_0 :
      forall s, exists l : list elt,
-        noredunA E.eq l /\
+        NoDupA E.eq l /\
         (forall x : elt, In x s <-> InA E.eq x l) /\ 
         cardinal s = length l.
   Proof. 
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index bcd966f9a8..4b98474b16 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -115,7 +115,7 @@ Module Raw (X: DecidableType).
 
   (** ** Proofs of set operation specifications. *)
 
-  Notation NoRedun := (noredunA X.eq).
+  Notation NoDup := (NoDupA X.eq).
   Notation In := (InA X.eq).
 
   Definition Equal s s' := forall a : elt, In a s <-> In a s'.
@@ -149,7 +149,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_1 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> In y (add x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -159,7 +159,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_2 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), In y s -> In y (add x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s).
   Proof.
   induction s. 
   simpl; intuition.
@@ -168,7 +168,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_3 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt),
+   forall (s : t) (Hs : NoDup s) (x y : elt),
    ~ X.eq x y -> In y (add x s) -> In y s.
   Proof.
   induction s. 
@@ -180,7 +180,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma add_unique :
-   forall (s : t) (Hs : NoRedun s)(x:elt), NoRedun (add x s).
+   forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s).
   Proof.
   induction s.  
   simpl; intuition.
@@ -197,7 +197,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_1 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), X.eq x y -> ~ In y (remove x s).
+   forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s).
   Proof.
   simple induction s. 
   simpl; red; intros; inversion H0.
@@ -208,7 +208,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_2 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt),
+   forall (s : t) (Hs : NoDup s) (x y : elt),
    ~ X.eq x y -> In y s -> In y (remove x s).
   Proof.
   simple induction s. 
@@ -219,7 +219,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_3 :
-   forall (s : t) (Hs : NoRedun s) (x y : elt), In y (remove x s) -> In y s.
+   forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s.
   Proof.
   simple induction s. 
   simpl; intuition.
@@ -228,7 +228,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma remove_unique :
-   forall (s : t) (Hs : NoRedun s) (x : elt), NoRedun (remove x s).
+   forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s).
   Proof.
   simple induction s.
   simpl; intuition.
@@ -239,7 +239,7 @@ Module Raw (X: DecidableType).
   eapply remove_3; eauto.
   Qed. 
 
-  Lemma singleton_unique : forall x : elt, NoRedun (singleton x).
+  Lemma singleton_unique : forall x : elt, NoDup (singleton x).
   Proof.
   unfold singleton; simpl; constructor; auto; intro H; inversion H.
   Qed.
@@ -255,7 +255,7 @@ Module Raw (X: DecidableType).
   unfold singleton; simpl; intuition.
   Qed. 
   
-  Lemma empty_unique : NoRedun empty.
+  Lemma empty_unique : NoDup empty.
   Proof.
   unfold empty; constructor.
   Qed.
@@ -287,13 +287,13 @@ Module Raw (X: DecidableType).
   unfold elements; auto.
   Qed.
  
-  Lemma elements_3 : forall (s : t) (Hs : NoRedun s), NoRedun (elements s).  
+  Lemma elements_3 : forall (s : t) (Hs : NoDup s), NoDup (elements s).  
   Proof. 
   unfold elements; auto.
   Qed.
 
   Lemma fold_1 :
-   forall (s : t) (Hs : NoRedun s) (A : Set) (i : A) (f : elt -> A -> A),
+   forall (s : t) (Hs : NoDup s) (A : Set) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
   induction s; simpl; auto; intros.
@@ -301,7 +301,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (union s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
   inversion_clear Hs.
@@ -310,7 +310,7 @@ Module Raw (X: DecidableType).
   Qed.
   
   Lemma union_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (union s s') -> In x s \/ In x s'.
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -322,7 +322,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_0 : 
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s \/ In x s' -> In x (union s s').
   Proof.
   unfold union; induction s; simpl; auto; intros.
@@ -338,25 +338,25 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma union_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
   Lemma union_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s' -> In x (union s s').
   Proof.
   intros; apply union_0; auto.
   Qed.
 
   Lemma inter_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (inter s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s').
   Proof.
   unfold inter; intros s.
   set (acc := nil (A:=elt)).
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   clearbody acc; generalize H; clear H; generalize acc; clear acc. 
   induction s; simpl; auto; intros.
   inversion_clear Hs.
@@ -366,12 +366,12 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma inter_0  :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s /\ In x s'.
   Proof.
   unfold inter; intros.
   set (acc := nil (A:=elt)) in *.
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   cut ((In x s /\ In x s') \/ In x acc).
     destruct 1; auto.
     inversion H1.
@@ -393,21 +393,21 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma inter_1  :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
   Lemma inter_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (inter s s') -> In x s'.
   Proof.
   intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ].
   Qed.
 
   Lemma inter_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> In x s' -> In x (inter s s').
   Proof.
   intros s s' Hs Hs' x.
@@ -415,7 +415,7 @@ Module Raw (X: DecidableType).
   intuition.
   unfold inter.
   set (acc := nil (A:=elt)) in *.
-  assert (NoRedun acc) by (unfold acc; auto).
+  assert (NoDup acc) by (unfold acc; auto).
   clearbody acc. 
   generalize H Hs' Hs; clear H Hs Hs'.
   generalize acc x s'; clear acc x s'.
@@ -441,7 +441,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma diff_unique :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'), NoRedun (diff s s').
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
   induction s'; simpl; auto; intros.
@@ -451,7 +451,7 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma diff_0 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> In x s /\ ~ In x s'.
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -468,21 +468,21 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma diff_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> In x s.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
   Lemma diff_2 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x (diff s s') -> ~ In x s'.
   Proof.
   intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. 
   Qed.
 
   Lemma diff_3 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s') (x : elt),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt),
    In x s -> ~ In x s' -> In x (diff s s').
   Proof.
   unfold diff; intros s s' Hs; generalize s Hs; clear Hs s.
@@ -494,7 +494,7 @@ Module Raw (X: DecidableType).
   Qed.  
   
   Lemma subset_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
    Subset s s' -> subset s s' = true.
   Proof.
   unfold subset, Subset; intros.
@@ -506,7 +506,7 @@ Module Raw (X: DecidableType).
   eapply diff_1; eauto.
   Qed.
 
-  Lemma subset_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'), 
+  Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'), 
      subset s s' = true -> Subset s s'.
   Proof.
   unfold subset, Subset; intros.
@@ -519,14 +519,14 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma equal_1 :
-   forall (s s' : t) (Hs : NoRedun s) (Hs' : NoRedun s'),
+   forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'),
    Equal s s' -> equal s s' = true.
   Proof.
   unfold Equal, equal; intros.
   apply andb_true_intro; split; apply subset_1; firstorder.
   Qed.
 
-  Lemma equal_2 : forall (s s' : t)(Hs : NoRedun s) (Hs' : NoRedun s'),  
+  Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'),  
      equal s s' = true -> Equal s s'.
   Proof.
   unfold Equal, equal; intros.
@@ -548,7 +548,7 @@ Module Raw (X: DecidableType).
   Qed.  
 
   Lemma cardinal_1 :
-   forall (s : t) (Hs : NoRedun s), cardinal s = length (elements s).
+   forall (s : t) (Hs : NoDup s), cardinal s = length (elements s).
   Proof.
   auto.
   Qed.
@@ -593,7 +593,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma filter_unique :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (filter f s).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s).
   Proof.
   simple induction s; simpl.
   auto.
@@ -690,7 +690,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma partition_aux_1 : 
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), 
     In x (fst (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -701,7 +701,7 @@ Module Raw (X: DecidableType).
   Qed. 
      
   Lemma partition_aux_2 : 
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool)(x:elt), 
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), 
     In x (snd (partition f s)) -> In x s.
   Proof.
   induction s; simpl; auto; intros.
@@ -712,7 +712,7 @@ Module Raw (X: DecidableType).
   Qed. 
   
   Lemma partition_unique_1 :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (fst (partition f s)).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -723,7 +723,7 @@ Module Raw (X: DecidableType).
   Qed.
   
   Lemma partition_unique_2 :
-   forall (s : t) (Hs : NoRedun s) (f : elt -> bool), NoRedun (snd (partition f s)).
+   forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -762,7 +762,7 @@ Module Make (X: DecidableType) <: S with Module E := X.
  Module E := X.
  Module Raw := Raw X. 
 
- Record slist : Set :=  {this :> Raw.t; unique : noredunA X.eq this}.
+ Record slist : Set :=  {this :> Raw.t; unique : NoDupA X.eq this}.
  Definition t := slist. 
  Definition elt := X.t.
  
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index c5edf1de47..9cc4d283ca 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -316,7 +316,7 @@ Ltac false_order := elimtype False; order.
 Notation In:=(InA eq).
 Notation Inf:=(lelistA lt).
 Notation Sort:=(sort lt).
-Notation NoRedun:=(noredunA eq).
+Notation NoDup:=(NoDupA eq).
 
 Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
 Proof. exact (InA_eqA eq_sym eq_trans). Qed.
@@ -343,10 +343,10 @@ Lemma Inf_alt :
  forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
 Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
 
-Lemma Sort_NoRedun : forall l, Sort l -> NoRedun l.
-Proof. exact (SortA_noredunA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
+Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
+Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
 
-Hint Resolve ListIn_In Sort_NoRedun Inf_lt. 
+Hint Resolve ListIn_In Sort_NoDup Inf_lt. 
 Hint Immediate In_eq Inf_lt. 
 
 End OrderedTypeFacts.
@@ -502,9 +502,9 @@ Module PairOrderedType(O:OrderedType).
     red; simpl; auto.
   Qed.
 
-  Lemma Sort_noredunA: forall l, Sort l -> noredunA eqk l.
+  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
   Proof. 
-  exact (SortA_noredunA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk).
+  exact (SortA_NoDupA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk).
   Qed.
 
   Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
diff --git a/theories/Lists/MoreList.v b/theories/Lists/MoreList.v
index 5def8d84a1..f4456646ea 100644
--- a/theories/Lists/MoreList.v
+++ b/theories/Lists/MoreList.v
@@ -477,6 +477,15 @@ Fixpoint remove (x : A) (l : list A){struct l} : list A :=
 
 End Remove.
 
+Section NoDuplicates.
+
+(** A list without redundancy. *)
+
+Inductive NoDup : list A -> Prop := 
+ | NoDup_nil : NoDup nil 
+ | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). 
+
+End NoDuplicates.
 
 End MoreLists.
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index c65ea35629..1ad10c9c57 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -44,20 +44,13 @@ Proof.
  firstorder; subst; auto.
 Qed.
 
-(** A list without redundancy. *)
-
-Inductive noredun : list A -> Prop := 
- | noredun_nil : noredun nil 
- | noredun_cons : forall x l, ~ In x l -> noredun l -> noredun (x::l). 
-
-
 (** Similarly, a list without redundancy modulo the equality over [A]. *)
 
-Inductive noredunA : list A -> Prop :=
-  | noredunA_nil : noredunA nil
-  | noredunA_cons : forall x l, ~ InA x l -> noredunA l -> noredunA (x::l).
+Inductive NoDupA : list A -> Prop :=
+  | NoDupA_nil : NoDupA nil
+  | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
 
-Hint Constructors noredunA.
+Hint Constructors NoDupA.
 
 
 (** Results concerning lists modulo [eqA] *)
@@ -147,7 +140,7 @@ intros; eapply SortA_InfA_InA; eauto.
 apply InA_InfA.
 Qed.
 
-Lemma SortA_noredunA : forall l, SortA l -> noredunA l.
+Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
 Proof.
  simple induction l; auto.
  intros x l' H H0.
@@ -158,9 +151,9 @@ Proof.
  elim (ltA_not_eqA H3); auto.
 Qed.
 
-Lemma noredunA_app : forall l l', noredunA l -> noredunA l' -> 
+Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> 
   (forall x, InA x l -> InA x l' -> False) -> 
-  noredunA (l++l').
+  NoDupA (l++l').
 Proof.
 induction l; simpl; auto; intros.
 inversion_clear H.
@@ -180,13 +173,13 @@ apply (H1 x); auto.
 Qed.
 
 
-Lemma noredunA_rev : forall l, noredunA l -> noredunA (rev l).
+Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
 Proof.
 induction l.
 simpl; auto.
 simpl; intros.
 inversion_clear H.
-apply noredunA_app; auto.
+apply NoDupA_app; auto.
 constructor; auto.
 intro H2; inversion H2.
 intros x.
@@ -244,6 +237,6 @@ End Remove.
 End Type_with_equality.
 
 Hint Constructors InA.
-Hint Constructors noredunA. 
+Hint Constructors NoDupA. 
 Hint Constructors sort.
 Hint Constructors lelistA.