remove warnings in Coq 8.8

Author: gmalecha

examples/ConsiderDemo.v

@@ -1,16 +1,16 @@
 Require NPeano.
 Import NPeano.Nat.
 Require Import ExtLib.Tactics.Consider.
+Require Import Coq.Bool.Bool.
+Require Import ExtLib.Data.Nat.
+
+Require Import Coq.omega.Omega.
 
 Set Implicit Arguments.
 Set Strict Implicit.
 
 (**  Some tests *)
 Section test.
-  Require Import NPeano Coq.Bool.Bool.
-  Require Import ExtLib.Data.Nat.
-
-  Require Import Omega.
   Goal forall x y z,  (ltb x y && ltb y z) = true ->
                  ltb x z = true.
   intros x y z.

theories/Core/RelDec.v

@@ -1,4 +1,5 @@
 Require Import Coq.Bool.Bool.
+Require Import Coq.Classes.RelationClasses.
 Require Coq.Setoids.Setoid.
 
 Set Implicit Arguments.
@@ -70,8 +71,6 @@ Section lemmas.
     exfalso. eapply (@rel_dec_correct _ _ _ rc) in Heqb. auto.
   Qed.
 
-  Require Import RelationClasses.
-
   Theorem rel_dec_sym : Symmetric eqt -> forall x y,
     x ?[ eqt ] y = y ?[ eqt ] x.
   Proof.

theories/Data/Graph/BuildGraph.v

@@ -1,3 +1,6 @@
+Require Import ExtLib.Structures.Monads.
+Require Import ExtLib.Data.Monads.StateMonad.
+
 Set Implicit Arguments.
 Set Strict Implicit.
 
@@ -18,8 +21,6 @@ Arguments addEdge {_} {_} {_} _ _ _.
 
 (** A State Monad simplifies things **)
 Section Monadic.
-  Require Import ExtLib.Structures.Monads.
-  Require Import ExtLib.Data.Monads.StateMonad.
   Variable m : Type -> Type.
   Context {Monad_m : Monad m}.
 

theories/Data/Graph/GraphAlgos.v

@@ -1,4 +1,5 @@
 Require Import Coq.Lists.List.
+Require Import Coq.PArith.BinPos.
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Data.Graph.Graph.
@@ -45,9 +46,8 @@ Section GraphAlgos.
 
     End monadic.
 
-    Require Import BinPos.
     Definition dfs (from : V) : list V :=
-      let count := Npos (List.fold_left (fun acc _ => BinPos.Psucc acc) (verticies g) 1%positive) in
+      let count := Npos (List.fold_left (fun acc _ => Pos.succ acc) (verticies g) 1%positive) in
       let res := runGFix (dfs' from nil) count in
       match res with
         | Diverge => (** This should never happen! **)

theories/Data/List.v

@@ -1,8 +1,10 @@
 Require Import Coq.Lists.List.
+Require Coq.Classes.EquivDec.
 Require Import ExtLib.Core.Type.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
+Require ExtLib.Data.Nat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Tactics.Injection.
 
@@ -45,7 +47,6 @@ Section type.
 End type.
 
 Section EqDec.
-  Require EquivDec.
   Variable T : Type.
   Variable EqDec_T : EquivDec.EqDec _ (@eq T).
 
@@ -155,9 +156,9 @@ Global Instance Monad_list : Monad list :=
   List.fold_right (fun x acc => f x ++ acc) nil x
 }.
 
-Section list.
-  Require ExtLib.Data.Nat.
 
+
+Section list.
   Inductive R_list_len {T} : list T -> list T -> Prop :=
   | R_l_len : forall n m, length n < length m -> R_list_len n m.
 

theories/Data/String.v

@@ -1,4 +1,8 @@
 Require Import Coq.Strings.String.
+Require Import Coq.Program.Program. 
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.Arith.Arith.
+
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Reducible.
@@ -71,8 +75,6 @@ Fixpoint string_cmp (l r : string) : comparison :=
   end.
 
 Section Program_Scope.
-  Require Import Program.
-  Import NPeano.Nat Arith.
   Variable modulus : nat.
   Hypothesis one_lt_mod : 1 < modulus.
 

theories/Programming/Show.v

@@ -1,3 +1,5 @@
+Require Coq.Strings.Ascii.
+Require Coq.Strings.String.
 Require Import Coq.Strings.String.
 Require Import Coq.Program.Wf.
 Require Import Coq.PArith.BinPos.
@@ -133,11 +135,10 @@ Section sum_Show.
         " "%char <<
         payload <<
         ")"%char.
-        
+
 End sum_Show.
 
 Section foldable_Show.
-  Require Import ExtLib.Structures.Reducible.
   Polymorphic Context {A:Type} {B:Type} {F : Foldable B A} {BS : Show A}.
 
   Global Polymorphic  Instance foldable_Show : Show B :=
@@ -154,51 +155,51 @@ Polymorphic Fixpoint iter_show (ss : list showM) : showM :=
 Section hiding_notation.
   Import ShowNotation.
   Local Open Scope show_scope.
-  Require Import Ascii.
-  Require Import String.
+  Import Ascii.
+  Import String.
 
-Global Instance unit_Show : Show unit :=
+  Global Instance unit_Show : Show unit :=
   { show u := "tt"%string }.
-Global Instance bool_Show : Show bool :=
+  Global Instance bool_Show : Show bool :=
   { show b := if b then "true"%string else "false"%string }.
-Global Instance ascii_Show : Show ascii :=
-  fun a =>  "'"%char << a << "'"%char.
-Global Instance string_Show : Show string :=
+  Global Instance ascii_Show : Show ascii :=
+    fun a =>  "'"%char << a << "'"%char.
+  Global Instance string_Show : Show string :=
   { show s := """"%char << s << """"%char }.
 
-Program Fixpoint nat_show (n:nat) {measure n} : showM :=
-  if Compare_dec.le_gt_dec n 9 then
-    inject (Char.digit2ascii n)
-  else
-    let n' := NPeano.Nat.div n 10 in
-    (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
-Next Obligation.
-  assert (NPeano.Nat.div n 10 < n) ; eauto.
-  eapply NPeano.Nat.div_lt.
-  inversion H; apply Lt.lt_O_Sn.
-  repeat constructor.
-Defined.
-Global Instance nat_Show : Show nat := { show := nat_show }.
-
-Global Instance Show_positive : Show positive :=
-  fun x => nat_show (Pos.to_nat x).
-
-Global Instance Show_Z : Show Z :=
-  fun x =>
-    match x with
+  Program Fixpoint nat_show (n:nat) {measure n} : showM :=
+    if Compare_dec.le_gt_dec n 9 then
+      inject (Char.digit2ascii n)
+    else
+      let n' := NPeano.Nat.div n 10 in
+      (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
+  Next Obligation.
+    assert (NPeano.Nat.div n 10 < n) ; eauto.
+    eapply NPeano.Nat.div_lt.
+    inversion H; apply Lt.lt_O_Sn.
+    repeat constructor.
+  Defined.
+  Global Instance nat_Show : Show nat := { show := nat_show }.
+
+  Global Instance Show_positive : Show positive :=
+    fun x => nat_show (Pos.to_nat x).
+
+  Global Instance Show_Z : Show Z :=
+    fun x =>
+      match x with
       | Z0 => "0"%char
       | Zpos p => show p
       | Zneg p => "-"%char << show p
-    end.
-
-Section pair_Show.
-  Polymorphic Definition pair_Show@{a m}
-              {A : Type@{a}} {B : Type@{a}} {AS:Show A} {BS:Show B}
-  : Show (A*B) :=
-    fun p =>
-      let (a,b) := p in
-      "("%char << show a << ","%char << show b << ")"%char.
-End pair_Show.
+      end.
+
+  Section pair_Show.
+    Polymorphic Definition pair_Show@{a m}
+                {A : Type@{a}} {B : Type@{a}} {AS:Show A} {BS:Show B}
+    : Show (A*B) :=
+      fun p =>
+        let (a,b) := p in
+        "("%char << show a << ","%char << show b << ")"%char.
+  End pair_Show.
 End hiding_notation.
 
 

theories/Recur/Measure.v

@@ -1,4 +1,5 @@
 Require Import Coq.Classes.RelationClasses.
+Require Coq.Arith.Wf_nat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -25,7 +26,6 @@ End parametric.
 
 (** A well-founded relation induced by a measure to nat **)
 Section measure.
-  Require Coq.Arith.Wf_nat.
   Context {T : Type}.
   Variable m : T -> nat.
 

theories/Structures/Reducible.v

@@ -1,5 +1,6 @@
-Require Import RelationClasses.
+Require Import Coq.Classes.RelationClasses.
 Require Import ExtLib.Structures.BinOps.
+Require Import ExtLib.Structures.Monad.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -12,32 +13,30 @@ Class Foldable (T E : Type) : Type :=
 
 Section RedFold.
   Variables T E : Type.
-  
+
   Global Instance Reducible_from_Foldable (R : Foldable T E) : Reducible T E | 100 :=
     fun A base single join =>
       @fold _ _ R A (fun x => join (single x)) base.
 End RedFold.
 
 Section foldM.
-  Require Import ExtLib.Structures.Monad.
   Context {T E : Type}.
   Context {Foldable_te : Foldable T E}.
   Context {m : Type -> Type}.
   Context {Monad_m : Monad m}.
 
   Definition foldM {A} (add : E -> A -> m A) (base : m A) (t : T) : m A :=
-    fold (fun x acc => bind acc (add x)) base t.  
+    fold (fun x acc => bind acc (add x)) base t.
 End foldM.
 
 Section reduceM.
-  Require Import ExtLib.Structures.Monad.
   Context {T E : Type}.
   Context {Reducible_te : Reducible T E}.
   Context {m : Type -> Type}.
   Context {Monad_m : Monad m}.
 
   Definition reduceM {A} (base : m A) (single : E -> m A) (join : A -> A -> m A)  (t : T) : m A :=
-    reduce base single (fun x y => bind x (fun x => bind y (fun y => join x y))) t.  
+    reduce base single (fun x y => bind x (fun x => bind y (fun y => join x y))) t.
 End reduceM.
 
 Section iterM.
@@ -46,8 +45,8 @@ Section iterM.
 
   Context {m : Type -> Type}.
   Context {Monad_m : Monad m}.
-  Context {Red_te : Reducible T E}. 
-  
+  Context {Red_te : Reducible T E}.
+
   Variable f : E -> m unit.
 
   Definition iterM : T -> m unit :=
@@ -60,7 +59,7 @@ Section Laws.
   Context (R : Reducible T E).
 
   Class ReducibleLaw : Prop :=
-    reduce_spec : forall A 
+    reduce_spec : forall A
       (unit : A)
       (single : E -> A)
       (join : A -> A -> A)

theories/Tactics/EqDep.v

@@ -1,5 +1,6 @@
 Require Import Coq.Classes.EquivDec.
 Require Import ExtLib.Structures.EqDep.
+Require Coq.Logic.Eqdep_dec.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -8,8 +9,6 @@ Section Classes.
   Context {A : Type}.
   Context {dec : EqDec A (@eq A)}.
 
-  Require Eqdep_dec.
-
   Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
     intros.
     eapply Eqdep_dec.UIP_dec. apply equiv_dec.