remove a host of warnings

tests/Test.v

@@ -12,6 +12,7 @@ Require Import Arith Bool.
 
 Set Implicit Arguments.
 
+Set Warnings "-notation-overridden".
 
 (******************************************************************)
 (** * Basics: definition of polymorphic lists and some operations *)
@@ -92,7 +93,7 @@ Delimit Scope list_scope with list.
 
 Bind Scope list_scope with list.
 
-Arguments list _%type_scope.
+Arguments list _%_type_scope.
 
 (** ** Facts about lists *)
 
@@ -211,7 +212,7 @@ Section Facts.
     now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
     rewrite <- IHl; auto.
   Qed.
-  Hint Resolve app_ass.
+  Hint Resolve app_ass : core.
 
   Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
   Proof.
@@ -362,15 +363,15 @@ Section Elts.
   Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A :=
     match n, l with
       | O, x :: l' => x
-      | O, other => default
+      | O, _other => default
       | S m, nil => default
       | S m, x :: t => nth m t default
     end.
 
   Fixpoint nth_ok (n:nat) (l:list A) (default:A) {struct l} : bool :=
     match n, l with
       | O, x :: l' => true
-      | O, other => false
+      | O, _other => false
       | S m, nil => false
       | S m, x :: t => nth_ok m t default
     end.
@@ -412,7 +413,7 @@ Section Elts.
   Proof.
     unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
     destruct l; simpl in |- *; [ inversion 2 | auto ].
-    destruct l as [| a l hl]; simpl in |- *.
+    destruct l as [| a l]; simpl in |- *.
     inversion 2.
     intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -568,8 +569,8 @@ Section Elts.
     induction l as [|y l].
     simpl; intros; split; [destruct 1 | apply Nat.lt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
-    rewrite Heq; intuition.
-    pose (IHl x). intuition.
+    rewrite Heq; intuition auto with *.
+    pose (IHl x). intuition auto with *.
   Qed.
 
   Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
@@ -783,7 +784,7 @@ Section ListOps.
       | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
       | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.
 
-    Hint Constructors Permutation.
+    Hint Constructors Permutation : core.
 
   (** Some facts about [Permutation] *)
 
@@ -818,7 +819,7 @@ Section ListOps.
       exact perm_trans.
     Qed.
 
-    Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
+    Hint Resolve Permutation_refl Permutation_sym Permutation_trans : core.
 
   (** Compatibility with others operations on lists *)
 
@@ -873,7 +874,7 @@ Section ListOps.
     apply perm_swap; auto.
     apply perm_skip; auto.
     Qed.
-    Hint Resolve Permutation_cons_app.
+    Hint Resolve Permutation_cons_app : core.
 
     Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
     Proof.
@@ -1072,7 +1073,7 @@ Section Map.
     rewrite IHl; auto.
   Qed.
 
-  Hint Constructors Permutation.
+  Hint Constructors Permutation : core.
 
   Lemma Permutation_map :
     forall l l', Permutation l l' -> Permutation (map l) (map l').
@@ -1588,19 +1589,19 @@ Section SetIncl.
   Variable A : Type.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
-  Hint Unfold incl.
+  Hint Unfold incl : core.
 
   Lemma incl_refl : forall l:list A, incl l l.
   Proof.
     auto.
   Qed.
-  Hint Resolve incl_refl.
+  Hint Resolve incl_refl : core.
 
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_tl.
+  Hint Immediate incl_tl : core.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
   Proof.
@@ -1611,13 +1612,13 @@ Section SetIncl.
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_appl.
+  Hint Immediate incl_appl : core.
 
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_appr.
+  Hint Immediate incl_appr : core.
 
   Lemma incl_cons :
     forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
@@ -1632,15 +1633,15 @@ Section SetIncl.
     now_show (In a0 l -> In a0 m).
     auto.
   Qed.
-  Hint Resolve incl_cons.
+  Hint Resolve incl_cons : core.
 
   Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
   Proof.
     unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
-  Hint Resolve incl_app.
+  Hint Resolve incl_app : core.
 
 End SetIncl.
 
@@ -1730,7 +1731,7 @@ End Cutting.
 
 Module ReDun.
 
-  Variable A : Type.
+  Parameter A : Type.
 
   Inductive NoDup : list A -> Prop :=
     | NoDup_nil : NoDup nil