From f82ed75cdaeda369bc96fc722ddfe52b27f8c124 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 7 Dec 2024 20:47:46 +0100
Subject: [PATCH] Address some deprecation warnings

---
 BigN/BigN.v                 |   6 +++---
 BigN/NMake.v                |   5 +++--
 BigN/Nbasic.v               |   6 +++---
 BigN/gen/NMake_gen.ml       |   6 +++---
 BigNumPrelude.v             |  16 ++++++++--------
 BigQ/BigQ.v                 |   3 ++-
 BigQ/QMake.v                |   6 +++---
 BigZ/BigZ.v                 |   7 ++++---
 BigZ/ZMake.v                |   2 +-
 CyclicDouble/DoubleAdd.v    |   4 ++--
 CyclicDouble/DoubleBase.v   |   5 ++---
 CyclicDouble/DoubleCyclic.v |   6 +++---
 CyclicDouble/DoubleDiv.v    |   4 ++--
 CyclicDouble/DoubleDivn1.v  |   4 ++--
 CyclicDouble/DoubleLift.v   |   4 ++--
 CyclicDouble/DoubleMul.v    |   4 ++--
 CyclicDouble/DoubleSqrt.v   |   4 ++--
 CyclicDouble/DoubleSub.v    |   4 ++--
 SpecViaQ/QSig.v             |   3 ++-
 SpecViaZ/.lia.cache         | Bin 4450 -> 2025 bytes
 SpecViaZ/NSig.v             |   3 ++-
 SpecViaZ/NSigNAxioms.v      |   3 ++-
 SpecViaZ/ZSig.v             |   3 ++-
 SpecViaZ/ZSigZAxioms.v      |   3 ++-
 plugin/bignums_syntax.ml    |   4 ++--
 25 files changed, 61 insertions(+), 54 deletions(-)

diff --git a/BigN/BigN.v b/BigN/BigN.v
index b1c0c93..fff3d4b 100644
--- a/BigN/BigN.v
+++ b/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 *)
diff --git a/BigN/NMake.v b/BigN/NMake.v
index 66f8be1..cfba61b 100644
--- a/BigN/NMake.v
+++ b/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.
 
diff --git a/BigN/Nbasic.v b/BigN/Nbasic.v
index 5e90137..ac2ebee 100644
--- a/BigN/Nbasic.v
+++ b/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.
diff --git a/BigN/gen/NMake_gen.ml b/BigN/gen/NMake_gen.ml
index e89e17b..4b3db11 100644
--- a/BigN/gen/NMake_gen.ml
+++ b/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.
 
diff --git a/BigNumPrelude.v b/BigNumPrelude.v
index b629a39..1708ebd 100644
--- a/BigNumPrelude.v
+++ b/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.
diff --git a/BigQ/BigQ.v b/BigQ/BigQ.v
index ab0e8fd..145ae72 100644
--- a/BigQ/BigQ.v
+++ b/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.
diff --git a/BigQ/QMake.v b/BigQ/QMake.v
index cb8cfcb..ad1d128 100644
--- a/BigQ/QMake.v
+++ b/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
diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v
index 0582395..68cce96 100644
--- a/BigZ/BigZ.v
+++ b/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.
diff --git a/BigZ/ZMake.v b/BigZ/ZMake.v
index b892fb6..ca188d8 100644
--- a/BigZ/ZMake.v
+++ b/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.
diff --git a/CyclicDouble/DoubleAdd.v b/CyclicDouble/DoubleAdd.v
index 1664f22..5f1e245 100644
--- a/CyclicDouble/DoubleAdd.v
+++ b/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.
diff --git a/CyclicDouble/DoubleBase.v b/CyclicDouble/DoubleBase.v
index 3959a98..4bf1de7 100644
--- a/CyclicDouble/DoubleBase.v
+++ b/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.
-
diff --git a/CyclicDouble/DoubleCyclic.v b/CyclicDouble/DoubleCyclic.v
index 4ccc19a..fff3073 100644
--- a/CyclicDouble/DoubleCyclic.v
+++ b/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.
 
diff --git a/CyclicDouble/DoubleDiv.v b/CyclicDouble/DoubleDiv.v
index 6bb78c6..1c441cd 100644
--- a/CyclicDouble/DoubleDiv.v
+++ b/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.
diff --git a/CyclicDouble/DoubleDivn1.v b/CyclicDouble/DoubleDivn1.v
index 9d0b354..f95a0b2 100644
--- a/CyclicDouble/DoubleDivn1.v
+++ b/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.
diff --git a/CyclicDouble/DoubleLift.v b/CyclicDouble/DoubleLift.v
index 75a6571..f868c3b 100644
--- a/CyclicDouble/DoubleLift.v
+++ b/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.
diff --git a/CyclicDouble/DoubleMul.v b/CyclicDouble/DoubleMul.v
index 8bcd050..d70f8e4 100644
--- a/CyclicDouble/DoubleMul.v
+++ b/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.
diff --git a/CyclicDouble/DoubleSqrt.v b/CyclicDouble/DoubleSqrt.v
index 4943436..dc26397 100644
--- a/CyclicDouble/DoubleSqrt.v
+++ b/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.
diff --git a/CyclicDouble/DoubleSub.v b/CyclicDouble/DoubleSub.v
index 8973b2b..e5136e3 100644
--- a/CyclicDouble/DoubleSub.v
+++ b/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.
diff --git a/SpecViaQ/QSig.v b/SpecViaQ/QSig.v
index 90cf7a0..d994090 100644
--- a/SpecViaQ/QSig.v
+++ b/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.
 
diff --git a/SpecViaZ/.lia.cache b/SpecViaZ/.lia.cache
index 988c28a26d4b3753dda8476b7753cb423cbe5765..9589a401f9ba64716effdd3dcd7759a01830a5bd 100644
GIT binary patch
delta 320
zcmaE)^pc;$IloYmfx+g%WJks{=Ay;ClN-4$C!gce6qxAX>@Z=$(!~=dI!v4}!C~U$
zS)6%%aPHEHAR#fXJRTqmC=DWk0u#7$xZr9gPG;jq;nr~HBFlc}&J%#@M%Yrwlg9-%
z3`hVCT+N$=tVNtJ32dRmM27`SfexG8%9kR5un;QvlP?`vQx<;|H^d&WHIvWtM<VNS
l;N_prG<lAI<K#*KVPt*N1R}U$W`o@FQy`WH#s@mU0RV3Mi~0Zn

literal 4450
zcmc&%Uucd|82{K?v(3j>V=}f2W*M?!w&Y@GCbPw4AvPf)OD>QUl0qT$O)akYW{bGN
zqFDKpmBPJ}6gT9KlnW8R=bYy`@1OIn?@#2bU*G$l_nh;4e$T)6yz!dhM<@HPKaRy>
z>w$T|K|(5Zr@6VH>9_f%QbWmJrG}D8rEt-bO7-K$8>f<V&Ck39ZWTW&)ALj^HFymR
zl30jmn>w#F1;}babeNDcndN~|Fo9@5kyJslNe?#**&2|{1@;kKGVG=$_{uQiD@#wN
zz(|^AuKv)<n#!?#5kUXtE)CnNmbTw5<Q3B~vlyr#L|2fDWzDL!i8fwyA9MG{Vq+!~
zqHA=7f?|5HiRk0)C`2^uO^C|YZ2B=hr#s&ZI^gr{3cE?840$a!4ipKBhaV7oMK0Ss
zqeH~phL|1*DIvIGU_vnGwADq1Fe;`@?2zotD5l=7uwt5I2stiE6_O#!NJjOMDQ7q)
z_aI|8B#bBgbr~jFv#6qMaJ>1r)s?6np`)`ztT)qe=Pj2ZZ>ko=#i%uz06`J79NzUt
zv^;>8J<w4~aJ5J>ak1o@Uq(wsSW7i-y;|ucT1%Z6?rT{pLtbkjIJV|PDb^i-U&67u
z2|YWZWenke=z+($;%qtxdX{9AHQxlJ>s_S?=!bx<z&C;`z;0^#a;`O!MRH{l0MjX#
zkVu%>&|LqDJ%1SncLARWf8B7l%I#F6o9kphrnc9A58B%eTR#(AdokHG9pBM16m3R1
zb=J}C)n1Jx#+LJ^6YSp$uyX_OmXO(A@syj6*|f~utgP&No~4!1^!-;>ri*>N^5s+Z
zWdc4d0O)O89QLJB`v>A9JdX--A#jQio@Wn2a20n)lQ8JRC1|qJ-*8(>J=dI+w0>{8
zUJ*Gil{73|#<V*?w-`82$d6XH)k!|FSI+5dUUhOz<73UDfiJ?now?89|D4MWCBd=~
z$>anpS#uW$xDz36-8`s=(2V_q6UMUYEnr*#oFKT&k<=09Y@8j|4A!cVi+Qu+9Lx<M
zeTcoO_IV`2RnL0!POPk1`79#=hS+00HnDcWwT(b8AsZLFw9&*e8I4!Ge}=LzX$o-l
zYnxizz`6)HO>o&UIg(m-B%E4tKeY@yK0hqGoYZH0Jt=3LHt^K|Jp`8*dzb>o;ZyHN
z15&WKi0nPkhglddI@?*ynVS!R!_aR^BB@e?=G_{fGyIbY*1>Z6q&YxHs~~uAh8r_{
ztT_cybL-b}=Gq93I^Y<=<$~Q2F6}PA7PQB>-Fbz^d#sJ6VaBxQTaO0Ho|@emg3D(k
zV&22HwnF_^qUH1X`ET4w?MBVIaU%HnOJAf%2zjsubA+zlvh%JUdcqPrKtkWzqkNI_
zdi#cerL2zf(H~|G-9L>!rB<%^_=8#6!7v-hl;%{yV!nSxqb78bt`(nnNqXff>|O)l
zgCVvjt<&^NK(^8mGYndiZXFZT`KtQR3kgjA9O5c`>4Gkx!j#jLkxJ2#O*}&B7EqEd
IB7U-|KR8gTT>t<8

diff --git a/SpecViaZ/NSig.v b/SpecViaZ/NSig.v
index 8406ce4..8493f0b 100644
--- a/SpecViaZ/NSig.v
+++ b/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.
 
diff --git a/SpecViaZ/NSigNAxioms.v b/SpecViaZ/NSigNAxioms.v
index 610d0f3..4d24b0b 100644
--- a/SpecViaZ/NSigNAxioms.v
+++ b/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] *)
 
diff --git a/SpecViaZ/ZSig.v b/SpecViaZ/ZSig.v
index 80c1486..a2d1770 100644
--- a/SpecViaZ/ZSig.v
+++ b/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.
 
diff --git a/SpecViaZ/ZSigZAxioms.v b/SpecViaZ/ZSigZAxioms.v
index abc2eae..97f50bd 100644
--- a/SpecViaZ/ZSigZAxioms.v
+++ b/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] *)
 
diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml
index cd0cd32..a96448c 100644
--- a/plugin/bignums_syntax.ml
+++ b/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