Merge pull request #96 from coq-community/rm_deprecations

Address some deprecation warnings

BigN/BigN.v

@@ -10,8 +10,8 @@
 
 (** Initial Author: Arnaud Spiwack *)
 
-Require Import Lia CyclicAxioms Ring63 NSig NSigNAxioms NMake
-  NProperties GenericMinMax.
+From Stdlib Require Import Lia CyclicAxioms Ring63 NProperties GenericMinMax.
+Require Import NSig NSigNAxioms NMake.
 Import Cyclic63.
 
 (** The following [BigN] module regroups both the operations and
@@ -44,7 +44,7 @@ Notation bigN := BigN.t.
 Bind Scope bigN_scope with bigN.
 Bind Scope bigN_scope with BigN.t.
 Bind Scope bigN_scope with BigN.t'.
-Arguments BigN.N0 _%int63.
+Arguments BigN.N0 _%_int63.
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)

BigN/NMake.v

@@ -16,8 +16,9 @@
     representation. The representation-dependent (and macro-generated) part
     is now in [NMake_gen]. *)
 
-Require Import Bool BigNumPrelude ZArith Lia Nnat CyclicAxioms DoubleType
-  Nbasic Wf_nat StreamMemo NSig NMake_gen.
+From Stdlib Require Import Bool ZArith Lia Nnat CyclicAxioms DoubleType.
+From Stdlib Require Import Wf_nat StreamMemo.
+Require Import BigNumPrelude Nbasic NSig NMake_gen.
 
 Module Make (W0:CyclicType) <: NType.
 

BigN/Nbasic.v

@@ -8,11 +8,11 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
+From Stdlib Require Import CyclicAxioms.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
-Require Import CyclicAxioms.
 Require Import DoubleCyclic.
 
 Arguments mk_zn2z_ops [t] ops.

BigN/gen/NMake_gen.ml

@@ -49,9 +49,9 @@ pr
 
 (** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)
 
-Require Import BigNumPrelude ZArith Lia CyclicAxioms
- DoubleType DoubleMul DoubleDivn1 DoubleBase DoubleCyclic Nbasic
- Wf_nat StreamMemo.
+From Stdlib Require Import ZArith Lia CyclicAxioms DoubleType Wf_nat StreamMemo.
+Require Import BigNumPrelude.
+Require Import DoubleMul DoubleDivn1 DoubleBase DoubleCyclic Nbasic.
 
 Local Close Scope Z.
 

BigNumPrelude.v

@@ -14,14 +14,14 @@
     numbers. *)
 
 
-Require Import ArithRing.
-Require Export ZArith.
-Require Export Znumtheory.
-Require Export Zpow_facts.
-Require Uint63.
-Require Import Lia.
-
-Declare ML Module "bignums_syntax_plugin:coq-bignums.plugin".
+From Stdlib Require Import ArithRing.
+From Stdlib Require Export ZArith.
+From Stdlib Require Export Znumtheory.
+From Stdlib Require Export Zpow_facts.
+From Stdlib Require Uint63.
+From Stdlib Require Import Lia.
+
+Declare ML Module "coq-bignums.plugin".
 
 (* *** Nota Bene ***
    All results that were general enough have been moved in ZArith.

BigQ/BigQ.v

@@ -10,8 +10,9 @@
 
 (** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
+From Stdlib Require Import Field Qfield Orders GenericMinMax.
 Require Export BigZ.
-Require Import Field Qfield QSig QMake Orders GenericMinMax.
+Require Import QSig QMake.
 
 (** We choose for BigQ an implemention with
     multiple representation of 0: 0, 1/0, 2/0 etc.

BigQ/QMake.v

@@ -10,9 +10,9 @@
 
 (** Initial authors : Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
-Require Import BigNumPrelude Lia.
-Require Import QArith Qcanon Qpower Qminmax.
-Require Import NSig ZSig QSig.
+From Stdlib Require Import Lia.
+From Stdlib Require Import QArith Qcanon Qpower Qminmax.
+Require Import BigNumPrelude NSig ZSig QSig.
 
 (** We will build rationals out of an implementation of integers [ZType]
     for numerators and an implementation of natural numbers [NType] for

BigZ/BigZ.v

@@ -8,8 +8,9 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
+From Stdlib Require Import ZProperties ZDivFloor Ring Lia.
 Require Export BigN.
-Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia.
+Require Import ZSig ZSigZAxioms ZMake.
 Import Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.
@@ -45,8 +46,8 @@ Notation bigZ := BigZ.t.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
-Arguments BigZ.Pos _%bigN.
-Arguments BigZ.Neg _%bigN.
+Arguments BigZ.Pos _%_bigN.
+Arguments BigZ.Neg _%_bigN.
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
 Local Notation "2" := BigZ.two : bigZ_scope.

BigZ/ZMake.v

@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.

CyclicDouble/DoubleAdd.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

CyclicDouble/DoubleBase.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 
 Local Open Scope Z_scope.
 
@@ -441,4 +441,3 @@ Section DoubleBase.
  End DoubleProof.
 
 End DoubleBase.
-

CyclicDouble/DoubleCyclic.v

@@ -10,9 +10,10 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
+From Stdlib Require Import CyclicAxioms.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 Require Import DoubleAdd.
 Require Import DoubleSub.
@@ -21,7 +22,6 @@ Require Import DoubleSqrt.
 Require Import DoubleLift.
 Require Import DoubleDivn1.
 Require Import DoubleDiv.
-Require Import CyclicAxioms.
 
 Local Open Scope Z_scope.
 

CyclicDouble/DoubleDiv.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 Require Import DoubleDivn1.
 Require Import DoubleAdd.

CyclicDouble/DoubleDivn1.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

CyclicDouble/DoubleLift.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

CyclicDouble/DoubleMul.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

CyclicDouble/DoubleSqrt.v

@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

CyclicDouble/DoubleSub.v

@@ -11,9 +11,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.

SpecViaQ/QSig.v

@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax.
+From Stdlib Require Import QArith Qpower Qminmax.
+From Stdlib Require Import Orders RelationPairs GenericMinMax.
 
 Open Scope Q_scope.
 

SpecViaZ/NSig.v

@@ -8,7 +8,8 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import BinInt DoubleBase.
+From Stdlib Require Import BinInt.
+Require Import DoubleBase.
 
 Open Scope Z_scope.
 

SpecViaZ/NSigNAxioms.v

@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith OrdersFacts Nnat NAxioms NSig Lia.
+From Stdlib Require Import ZArith OrdersFacts Nnat NAxioms Lia.
+Require Import NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 

SpecViaZ/ZSig.v

@@ -8,7 +8,8 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import BinInt DoubleBase.
+From Stdlib Require Import BinInt.
+Require Import DoubleBase.
 
 Open Scope Z_scope.
 

SpecViaZ/ZSigZAxioms.v

@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia.
+From Stdlib Require Import Bool ZArith OrdersFacts Nnat ZAxioms Lia.
+Require Import ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 

plugin/bignums_syntax.ml

@@ -108,8 +108,8 @@ let word_of_pos_bigint ?loc hght n =
   decomp hght n
 
 let nat_of_int ?loc n =
-  let ref_O = DAst.make ?loc (GRef (Coqlib.lib_ref "num.nat.O", None)) in
-  let ref_S = DAst.make ?loc (GRef (Coqlib.lib_ref "num.nat.S", None)) in
+  let ref_O = DAst.make ?loc (GRef (Rocqlib.lib_ref "num.nat.O", None)) in
+  let ref_S = DAst.make ?loc (GRef (Rocqlib.lib_ref "num.nat.S", None)) in
   let rec mk_nat acc n =
     if Int.equal n 0 then acc
     else