Merge pull request #27 from rocq-community/mc1415

Adapt to math-comp/math-comp#1415

Author: proux01

src/extraction/axioms16.v

@@ -1,9 +1,7 @@
-From Coq
-     Require Import ZArith.ZArith Extraction.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp Require Import ssrbool eqtype ssrnat seq fintype ssrfun tuple.
-From Bits
-     Require Import bits.
+From Coq Require Import ZArith.ZArith Extraction.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
+From mathcomp Require Import eqtype ssrnat seq fintype tuple.
+From Bits Require Import bits.
 
 (* TODO:
      * Complete missing lemmas

src/extraction/axioms32.v

@@ -1,9 +1,7 @@
-From Coq
-     Require Import ZArith.ZArith Extraction.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp Require Import ssrbool eqtype ssrnat seq fintype ssrfun tuple.
-From Bits
-     Require Import bits.
+From Coq Require Import ZArith.ZArith Extraction.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
+From mathcomp Require Import eqtype ssrnat seq fintype tuple.
+From Bits Require Import bits.
 
 (* TODO:
      * Complete missing lemmas

src/extraction/axioms8.v

@@ -1,9 +1,7 @@
-From Coq
-     Require Import ZArith.ZArith Extraction.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp Require Import ssrbool eqtype ssrnat seq fintype ssrfun tuple.
-From Bits
-     Require Import bits.
+From Coq Require Import ZArith.ZArith Extraction.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
+From mathcomp Require Import eqtype ssrnat seq fintype tuple.
+From Bits Require Import bits.
 
 (* TODO:
      * Complete missing lemmas

src/spec/operations.v

@@ -3,9 +3,7 @@
   For proofs of properties of operations see bitsopsprops.v
   ===========================================================================*)
 
-Require Import mathcomp.ssreflect.ssreflect.
-
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq tuple.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq tuple.
 Require Import spec.
 
 Set Implicit Arguments.

src/spec/operations/properties.v

@@ -3,9 +3,7 @@
   ===========================================================================*)
 From Coq Require Import Ring_theory.
 From HB Require Import structures.
-Require Import mathcomp.ssreflect.ssreflect.
-
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
 Require Import ssrextra.tuple ssrextra.nat.
 Require Import spec spec.properties operations.
 

src/spec/spec.v

@@ -12,10 +12,8 @@
   Proofs of properties of operations can be found in bitsopsprops.v
   ===========================================================================*)
 
-From Coq
-    Require Import ZArith.ZArith Strings.String.
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp.
+From Coq Require Import ZArith.ZArith Strings.String.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp.
 
 (* We represent n-bit words by a tuple of booleans, least-significant
 bit at the head DWORDorBYTE is especially useful for multi-mode

src/spec/spec/properties.v

@@ -3,9 +3,7 @@
   ===========================================================================*)
 From Coq Require Import ZArith.ZArith.
 (*Require Import common.tuplehelp common.nathelp.*)
-From mathcomp Require Import ssreflect.
-
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg.
 From mathcomp Require Import ring.
 Require Import ssrextra.nat ssrextra.tuple.
 Require Import spec.spec.

src/ssrextra/nat.v

@@ -1,9 +1,7 @@
 (*---------------------------------------------------------------------------
     Various helpers for halving, double and powers of 2
   ---------------------------------------------------------------------------*)
-Require Import mathcomp.ssreflect.ssreflect.
-
-From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

src/ssrextra/tuple.v

@@ -1,8 +1,6 @@
 (* Additional lemmas about tuples *)
 From Coq Require Import Setoid.
-Require Import mathcomp.ssreflect.ssreflect.
-
-From mathcomp Require Import ssrbool ssrnat eqtype seq fintype tuple.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq fintype tuple.
 
 Lemma mapCons {n A B} (f: A -> B) b (p: n.-tuple A) :
   map_tuple f [tuple of b :: p] = [tuple of f b :: map_tuple f p].