diff --git a/.github/workflows/latest.yml b/.github/workflows/latest.yml
index 507ed0c413..c23fea39c9 100644
--- a/.github/workflows/latest.yml
+++ b/.github/workflows/latest.yml
@@ -16,10 +16,10 @@ jobs:
       target: ${{ matrix.target }}
       os: linux
       jobs: 4
-      opamroot: /home/coq/.opam
+      opamroot: /home/rocq/.opam
       configopts: -ignore-coq-version
     container:
-      image: coqorg/coq:latest-ocaml-4.14-flambda
+      image: rocq/rocq-prover:latest
       options: --user root
     steps:
       - name: Checkout
@@ -27,7 +27,7 @@ jobs:
         with:
           submodules: true
       - name: OPAM dependencies
-        run: tools/runner.sh opam_install menhir
+        run: tools/runner.sh opam_install coq menhir
       - name: Configure
         run: tools/runner.sh configure
       - name: Build
diff --git a/.github/workflows/oldest.yml b/.github/workflows/oldest.yml
index 04fac4f7be..b79832ed59 100644
--- a/.github/workflows/oldest.yml
+++ b/.github/workflows/oldest.yml
@@ -19,7 +19,7 @@ jobs:
       opamroot: /home/coq/.opam
       configopts: -ignore-coq-version
     container:
-      image: coqorg/coq:8.13
+      image: coqorg/coq:8.15
       options: --user root
     steps:
       - name: Checkout
diff --git a/Makefile b/Makefile
index 0d4d243411..1e5f0ecaf5 100644
--- a/Makefile
+++ b/Makefile
@@ -61,11 +61,14 @@ endif
 # deprecated-since-8.20
 #    renamings performed in Coq's standard library;
 #    using the new names would break compatibility with earlier Coq versions.
+# deprecated-from-Coq
+#    Rocq wants "From Stdlib Require" while Coq wants "From Coq Require".
 
 COQCOPTS ?= \
   -w -unused-pattern-matching-variable \
   -w -deprecated-since-8.19 \
-  -w -deprecated-since-8.20
+  -w -deprecated-since-8.20 \
+  -w -deprecated-from-Coq
 
 cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
@@ -73,17 +76,20 @@ MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
 # Flocq and Menhirlib run into other renaming issues.
 # These warnings can only be addressed upstream.
 
-flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
-MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
+flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
+MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
 
 # For the extraction phase, we silence other warnings:
 # change-dir-deprecated:
 #    warning introduced in 8.20, no alternative before 8.20
 # extraction-default-directory:
 #    warning introduced in 8.20, no alternative before 8.20
+# deprecated-from-Coq:
+#    see above
 COQEXTRACTOPTS ?= \
   -w -change-dir-deprecated \
-  -w -extraction-default-directory
+  -w -extraction-default-directory \
+  -w -deprecated-from-Coq
 
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally
diff --git a/Makefile.extr b/Makefile.extr
index 688e45f330..afb6187697 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -72,6 +72,7 @@ EXTRWARNINGS=$(WARNINGS) \
   -w -ambiguous-name \
   -w -open-shadow-identifier \
   -w -open-shadow-label-constructor \
+  -w -unreachable-case \
   -w -unused-module \
   -w -unused-functor-parameter
 
diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index e1809aba4f..e117625486 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -16,8 +16,8 @@
 
 (** Architecture-dependent parameters for AArch64 *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := true.
 
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index b351c0aa52..332e849522 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -12,8 +12,8 @@
 
 (** Translation from Mach to AArch64. *)
 
-Require Import Recdef Coqlib Zwf Zbits.
-Require Import Errors AST Integers Floats Op.
+From Coq Require Import Recdef Zwf.
+Require Import Zbits Coqlib Errors AST Integers Floats Op.
 Require Import Locations Mach Asm.
 Require SelectOp.
 
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 93d64b5372..7c73138cbc 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -12,8 +12,9 @@
 
 (** Correctness proof for AArch64 code generation: auxiliary results. *)
 
-Require Import Recdef Coqlib Zwf Zbits.
-Require Import Maps Errors AST Integers Floats Values Memory Globalenvs.
+From Coq Require Import Recdef Zwf.
+Require Import Zbits Coqlib Maps Errors.
+Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Mach Asm Conventions.
 Require Import Asmgen.
 Require Import Asmgenproof0.
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v
index 1996f6a1a5..7ef2fb64af 100644
--- a/aarch64/Builtins1.v
+++ b/aarch64/Builtins1.v
@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type := .
diff --git a/aarch64/CombineOpproof.v b/aarch64/CombineOpproof.v
index 57778a67ef..1ed388b453 100644
--- a/aarch64/CombineOpproof.v
+++ b/aarch64/CombineOpproof.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib.
 Require Import AST Integers Values Memory.
 Require Import Op Registers RTL.
diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v
index f9b9fd791b..3687a744ad 100644
--- a/aarch64/Machregs.v
+++ b/aarch64/Machregs.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Decidableplus Maps.
 Require Import AST Op.
 
diff --git a/arm/Archi.v b/arm/Archi.v
index 2987b06dd8..687053f3be 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for ARM *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := false.
 
diff --git a/arm/Builtins1.v b/arm/Builtins1.v
index 1996f6a1a5..7ef2fb64af 100644
--- a/arm/Builtins1.v
+++ b/arm/Builtins1.v
@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type := .
diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v
index c8b332081e..ffdd86fa99 100644
--- a/arm/CombineOpproof.v
+++ b/arm/CombineOpproof.v
@@ -13,15 +13,9 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
-Require Import FunInd.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+From Coq Require Import FunInd.
+Require Import Coqlib AST Integers Values Memory.
+Require Import Op Registers RTL.
 Require Import CSEdomain.
 Require Import CombineOp.
 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index b61094a206..ab03af9a8e 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -10,12 +10,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
+From Coq Require Import String.
+Require Import Coqlib Decidableplus Maps.
+Require Import AST Op.
 
 (** ** Machine registers *)
 
diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v
index a82c082c87..745983c8c3 100644
--- a/arm/SelectLongproof.v
+++ b/arm/SelectLongproof.v
@@ -12,7 +12,8 @@
 
 (** Instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Integers Floats Errors.
+From Coq Require Import String.
+Require Import Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
diff --git a/backend/Allocation.v b/backend/Allocation.v
index ae4950ff38..07fb61559e 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -12,7 +12,8 @@
 
 (** Register allocation by external oracle and a posteriori validation. *)
 
-Require Import FSets FSetAVLplus.
+From Coq Require Import FSets.
+Require Import FSetAVLplus.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Lattice Kildall Memdata.
 Require Archi.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index d673810c6c..43fdb40767 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -13,8 +13,7 @@
 (** Correctness proof for the [Allocation] pass (validated translation from
   RTL to LTL). *)
 
-Require Import FunInd.
-Require Import FSets.
+From Coq Require Import FunInd FSets.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Linking Lattice Kildall.
 Require Import Values Memory Globalenvs Events Smallstep.
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 4231d861b7..b9979ddd1e 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -12,7 +12,7 @@
 
 (** Computation of resource bounds for Linear code. *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Ordered.
 Require Intv.
 Require Import AST.
diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v
index 303fcb646f..add676e7e3 100644
--- a/backend/CleanupLabels.v
+++ b/backend/CleanupLabels.v
@@ -20,7 +20,7 @@
   better-looking, the present pass removes labels that cannot be
   branched to. *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Ordered.
 Require Import Linear.
 
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index fb8e57b751..bfb872220f 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness proof for clean-up of labels *)
 
-Require Import FSets.
+From Coq Require Import FSets.
 Require Import Coqlib Ordered Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 52a9e3753a..f020318a1f 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -12,7 +12,7 @@
 
 (** Elimination of unneeded computations over RTL: correctness proof. *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Values Memory Builtins Globalenvs Events Smallstep.
diff --git a/backend/Inliningaux.mli b/backend/Inliningaux.mli
new file mode 100644
index 0000000000..a5f2666012
--- /dev/null
+++ b/backend/Inliningaux.mli
@@ -0,0 +1,19 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Inlining heuristics *)
+
+type inlining_info
+
+val inlining_analysis: RTL.program -> inlining_info
+
+val should_inline: inlining_info -> AST.ident -> RTL.coq_function -> bool
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 2cfa4d3c8a..fbfe01e8cc 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -12,7 +12,7 @@
 
 (** Linearization of the control-flow graph: translation from LTL to Linear *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Maps Ordered Errors Lattice Kildall.
 Require Import AST Op Locations LTL Linear.
 
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index b065238cde..e2c137801d 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness proof for code linearization *)
 
-Require Import FSets.
+From Coq Require Import FSets.
 Require Import Coqlib Maps Ordered Errors Lattice Kildall Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
diff --git a/backend/Locations.v b/backend/Locations.v
index 6c87c17545..0a9456ae78 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -13,12 +13,9 @@
 (** Locations are a refinement of RTL pseudo-registers, used to reflect
   the results of register allocation (file [Allocation]). *)
 
-Require Import OrderedType.
-Require Import Coqlib.
-Require Import Maps.
-Require Import Ordered.
-Require Import AST.
-Require Import Values.
+From Coq Require Import OrderedType.
+Require Import Coqlib Maps Ordered.
+Require Import AST Values.
 Require Export Machregs.
 
 (** * Representation of locations *)
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 889c55f1f5..f0dd2604b5 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -12,7 +12,8 @@
 
 (** Correctness proof for RTL generation. *)
 
-Require Import Wellfounded Coqlib Maps AST Linking.
+From Coq Require Import Wellfounded.
+Require Import Coqlib Maps AST Linking.
 Require Import Integers Values Memory Events Smallstep Globalenvs.
 Require Import Switch Registers Cminor Op CminorSel RTL.
 Require Import RTLgen RTLgenspec.
diff --git a/backend/Registers.v b/backend/Registers.v
index 7f7ecb6089..88c3539bdd 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -17,12 +17,9 @@
   intermediate language.  We also define finite sets and finite maps
   over pseudo-registers. *)
 
-Require Import Coqlib.
-Require Import AST.
-Require Import Maps.
-Require Import Ordered.
-Require FSetAVL.
-Require Import Values.
+From Coq Require FSetAVL.
+Require Import Coqlib Maps Ordered.
+Require Import AST Values.
 
 Definition reg: Type := positive.
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 9d581ec9c3..89b702f0d7 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -12,7 +12,8 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import Zquot Coqlib Zbits.
+From Coq Require Import Zquot.
+Require Import Coqlib Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
diff --git a/backend/Selection.v b/backend/Selection.v
index 2715399145..bd4a163592 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -22,7 +22,7 @@
   Instruction selection proceeds by bottom-up rewriting over expressions.
   The source language is Cminor and the target language is CminorSel. *)
 
-Require String.
+From Coq Require String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Globalenvs Builtins Switch.
 Require Cminor.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index e4395a9e02..392044fecb 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps.
 Require Import AST Linking Errors Integers.
 Require Import Values Memory Builtins Events Globalenvs Smallstep.
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index ca4af57289..15877223c2 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -12,7 +12,7 @@
 
 (** Instruction selection for 64-bit integer operations *)
 
-Require String.
+From Coq Require String.
 Require Import Coqlib.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index 32db4861d8..1a8c829a78 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Floats.
 Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index 265e06ba55..5b1b6e9697 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -12,7 +12,7 @@
 
 (** Branch tunneling (optimization of branches to branches). *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps UnionFind.
 Require Import AST.
 Require Import LTL.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 68913fc939..c05ec20e98 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness proof for the branch tunneling optimization. *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps UnionFind.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 8ac7c4ce5a..dbcf3b5413 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -12,7 +12,8 @@
 
 (** Elimination of unreferenced static definitions *)
 
-Require Import FSets Coqlib Maps Ordered Iteration Errors.
+From Coq Require Import FSets.
+Require Import Coqlib Maps Ordered Iteration Errors.
 Require Import AST Linking.
 Require Import Op Registers RTL.
 
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index df249d7551..9e1bf972f1 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -12,7 +12,8 @@
 
 (** Elimination of unreferenced static definitions *)
 
-Require Import FSets Coqlib Maps Ordered Iteration Errors.
+From Coq Require Import FSets.
+Require Import Coqlib Maps Ordered Iteration Errors.
 Require Import AST Linking.
 Require Import Integers Values Memory Globalenvs Events Smallstep.
 Require Import Op Registers RTL.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 3cdfbe4e4d..11807d02e4 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps Integers Floats Lattice Kildall.
 Require Import Compopts AST Linking.
 Require Import Values Memory Globalenvs Builtins Events.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 769e232f2b..c4daabac9c 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -10,8 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import FunInd.
-Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
+From Coq Require Import FunInd Zwf.
+Require Import Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index b6d8754339..c744416247 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -12,9 +12,8 @@
 
 (** Animating the CompCert C semantics *)
 
-Require Import FunInd.
-Require Import Axioms Classical.
-Require Import String Coqlib Decidableplus.
+From Coq Require Import FunInd Classical String.
+Require Import Axioms Coqlib Decidableplus.
 Require Import Errors Maps Integers Floats.
 Require Import AST Values Memory Events Globalenvs Builtins Determinism.
 Require Import Ctypes Cop Csyntax Csem.
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 1b031866e8..bfab7f098f 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -12,7 +12,7 @@
 
 (** Translation from Csharpminor to Cminor. *)
 
-Require Import FSets FSetAVL Orders Mergesort.
+From Coq Require Import FSets FSetAVL Orders Mergesort.
 Require Import Coqlib Maps Ordered Errors Integers Floats.
 Require Import AST Linking.
 Require Import Csharpminor Cminor.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index b299cd08ca..9fc50228e0 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -12,8 +12,8 @@
 
 (** Correctness proof for Cminor generation. *)
 
-Require Import Coq.Program.Equality FSets Permutation.
-Require Import FSets FSetAVL Orders Mergesort.
+From Coq Require Import Program.Equality Permutation Mergesort.
+From Coq Require Import Orders FSets FSetAVL.
 Require Import Coqlib Maps Ordered Errors Integers Floats.
 Require Intv.
 Require Import AST Linking.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 578615db0c..2b95fec18b 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -16,23 +16,10 @@
 
 (** A deterministic evaluation strategy for C. *)
 
-Require Import Axioms.
-Require Import Classical.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
+From Coq Require Import Classical.
+Require Import Axioms Coqlib Errors Maps.
+Require Import Integers Floats Values AST Memory Events Globalenvs Smallstep.
+Require Import Ctypes Cop Csyntax Csem.
 
 Section STRATEGY.
 
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index d5f3a4571d..df299154df 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -16,7 +16,7 @@
 
 (** Typing rules and type-checking for the Compcert C language *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Maps Integers Floats Errors.
 Require Import AST Linking.
 Require Import Values Memory Globalenvs Builtins Events.
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index e38652e0e1..6751e14326 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -12,7 +12,8 @@
 
 (** Compile-time evaluation of initializers for global C variables. *)
 
-Require Import Zwf Coqlib Maps.
+From Coq Require Import Zwf.
+Require Import Coqlib Maps.
 Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep.
 Require Import Ctypes Cop Csyntax Csem.
 Require Import Initializers.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index f49716951d..04e0d5a341 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness proof for expression simplification. *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps Errors Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index eec6ca4b14..9c1ba59642 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -13,8 +13,7 @@
 (** Pulling local scalar variables whose address is not taken
   into temporary variables. *)
 
-Require Import FSets.
-Require FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Ordered Errors.
 Require Import AST Linking.
 Require Import Ctypes Cop Clight.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 3eda31a3e6..da5bc5472d 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -12,7 +12,7 @@
 
 (** Semantic preservation for the SimplLocals pass. *)
 
-Require Import FSets.
+From Coq Require Import FSets.
 Require Import Coqlib Errors Ordered Maps Integers Floats.
 Require Import AST Linking.
 Require Import Values Memory Globalenvs Events Smallstep.
diff --git a/common/AST.v b/common/AST.v
index 658d9470d5..007d44afdb 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -17,7 +17,7 @@
 (** This file defines a number of data types and operations used in
   the abstract syntax trees of many of the intermediate languages. *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Maps Errors Integers Floats.
 Require Archi.
 
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 1f7f62263b..822b08832f 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -16,13 +16,9 @@
 
 (** Whole-program behaviors *)
 
-Require Import Classical.
-Require Import ClassicalEpsilon.
+From Coq Require Import Classical ClassicalEpsilon.
 Require Import Coqlib.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Integers.
-Require Import Smallstep.
+Require Import Events Globalenvs Integers Smallstep.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
diff --git a/common/Builtins.v b/common/Builtins.v
index f89b2af84b..0d50385f8f 100644
--- a/common/Builtins.v
+++ b/common/Builtins.v
@@ -16,7 +16,8 @@
 
 (** Known built-in functions *)
 
-Require Import String Coqlib.
+From Coq Require Import String.
+Require Import Coqlib.
 Require Import AST Integers Floats Values.
 Require Export Builtins0 Builtins1.
 
diff --git a/common/Builtins0.v b/common/Builtins0.v
index 1d2da3a72d..e1fc201573 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -16,7 +16,8 @@
 
 (** Associating semantics to built-in functions *)
 
-Require Import String Coqlib.
+From Coq Require Import String.
+Require Import Coqlib.
 Require Import AST Integers Floats Values Memdata.
 Local Open Scope asttyp_scope.
 
diff --git a/common/Determinism.v b/common/Determinism.v
index c8c907824e..45fe8bf7fc 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -17,14 +17,9 @@
 (** Characterization and properties of deterministic external worlds
   and deterministic semantics *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Behaviors.
+Require Import AST Integers Events Globalenvs Smallstep Behaviors.
 
 (** * Deterministic worlds *)
 
diff --git a/common/Errors.v b/common/Errors.v
index d376efe85f..a3e21b4db5 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -16,7 +16,7 @@
 
 (** Error reporting and the error monad. *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib.
 
 Close Scope string_scope.
diff --git a/common/Events.v b/common/Events.v
index 59fce81bfc..798ba568c6 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -16,16 +16,10 @@
 
 (** Observable events, execution traces, and semantics of external calls. *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib.
 Require Intv.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Builtins.
+Require Import AST Integers Floats Values Memory Globalenvs Builtins.
 Local Open Scope asttyp_scope.
 
 (** Backwards compatibility for Hint Rewrite locality attributes. *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 92ee8498b2..7356ca31f2 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -34,8 +34,7 @@
   place during program linking and program loading in a real operating
   system. *)
 
-Require Import Recdef.
-Require Import Zwf.
+From Coq Require Import Recdef Zwf.
 Require Import Axioms Coqlib Errors Maps AST Linking.
 Require Import Integers Floats Values Memory.
 
diff --git a/common/Memdata.v b/common/Memdata.v
index cf43589c7a..be8783d742 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -17,13 +17,9 @@
 
 (** In-memory representation of values. *)
 
-Require Import Coqlib.
-Require Import Zbits.
+Require Import Coqlib Zbits Integers Floats.
 Require Archi.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
+Require Import AST Values.
 
 (** * Properties of memory chunks *)
 
diff --git a/common/Memory.v b/common/Memory.v
index 786bc8597c..7b36ec5a21 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -27,18 +27,11 @@
 - [free]: invalidate a memory block.
 *)
 
-Require Import Zwf.
-Require Import Axioms.
-Require Import Coqlib.
+From Coq Require Import Zwf.
 Require Intv.
-Require Import Maps.
 Require Archi.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Export Memdata.
-Require Export Memtype.
+Require Import Axioms Coqlib Maps Integers Floats AST Values.
+Require Export Memdata Memtype.
 
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.
diff --git a/common/Memtype.v b/common/Memtype.v
index 7bf19347ab..188aa04ee0 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -24,12 +24,8 @@
 - [free]: invalidate a memory block.
 *)
 
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memdata.
+Require Import Coqlib Integers Floats.
+Require Import AST Values Memdata.
 
 (** Memory states are accessed by addresses [b, ofs]: pairs of a block
   identifier [b] and a byte offset [ofs] within that block.
diff --git a/common/Separation.v b/common/Separation.v
index 2ba6e77bb3..6658e37cba 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -30,7 +30,7 @@
   frame rule; instead, a weak form of the frame rule is provided
   by the lemmas that help us reason about the logical assertions. *)
 
-Require Import Setoid Program.Basics.
+From Coq Require Import Setoid Program.Basics.
 Require Import Coqlib Decidableplus.
 Require Import AST Integers Values Memory Events Globalenvs.
 
diff --git a/common/Smallstep.v b/common/Smallstep.v
index c7efcc903a..24e1b8eb05 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -20,12 +20,8 @@
   the one-step transition relations that are used to specify
   operational semantics in small-step style. *)
 
-Require Import Relations.
-Require Import Wellfounded.
-Require Import Coqlib.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Integers.
+From Coq Require Import Relations Wellfounded.
+Require Import Coqlib Events Globalenvs Integers.
 
 Set Implicit Arguments.
 
diff --git a/common/Subtyping.v b/common/Subtyping.v
index 8e5d9361e2..83571be555 100644
--- a/common/Subtyping.v
+++ b/common/Subtyping.v
@@ -16,7 +16,8 @@
 
 (* A solver for subtyping constraints. *)
 
-Require Import Recdef Coqlib Maps Errors.
+From Coq Require Import Recdef.
+Require Import Coqlib Maps Errors.
 
 Local Open Scope nat_scope.
 Local Open Scope error_monad_scope.
diff --git a/common/Switch.v b/common/Switch.v
index 23f9dd3e2b..05d86ec58a 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -17,11 +17,8 @@
 (** Multi-way branches (``switch'' statements) and their compilation
     to comparison trees. *)
 
-Require Import EqNat.
-Require Import Coqlib.
-Require Import Maps.
-Require Import Integers.
-Require Import Values.
+From Coq Require Import EqNat.
+Require Import Coqlib Maps Integers Values.
 
 (** A multi-way branch is composed of a list of (key, action) pairs,
   plus a default action.  *)
diff --git a/common/Unityping.v b/common/Unityping.v
index 1089b3599c..1d46cc6408 100644
--- a/common/Unityping.v
+++ b/common/Unityping.v
@@ -16,7 +16,8 @@
 
 (* A solver for unification constraints. *)
 
-Require Import Recdef Coqlib Maps Errors.
+From Coq Require Import Recdef.
+Require Import Coqlib Maps Errors.
 
 Local Open Scope nat_scope.
 Local Open Scope error_monad_scope.
diff --git a/common/Values.v b/common/Values.v
index 935117d37c..59d851305d 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -17,10 +17,7 @@
 (** This module defines the type of values that is used in the dynamic
   semantics of all our intermediate languages. *)
 
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
+Require Import Coqlib AST Integers Floats.
 
 Definition block : Type := positive.
 Definition eq_block := peq.
diff --git a/configure b/configure
index a26193ff20..9b1102d140 100755
--- a/configure
+++ b/configure
@@ -502,19 +502,24 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc --print-version 2>/dev/null | tr -d '\r' | cut -d' ' -f1)
 case "$coq_ver" in
-  8.13.0|8.13.1|8.13.2|8.14.0|8.14.1|8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1)
+  8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1|9.0.0)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.13.0 and 8.20.1"
+            echo "Error: CompCert requires a version of Coq between 8.15 and 9.0"
             missingtools=true
         fi;;
   "")
         echo "NOT FOUND"
-        echo "Error: make sure Coq is installed."
+        rocq_ver=$(${COQBIN}rocq --print-version 2>/dev/null | tr -d '\r' | cut -d' ' -f1)
+        case "$rocq_ver" in
+            "") echo "Error: make sure Coq is installed.";;
+             *) echo "Rocq prover version $rocq_ver found."
+                echo "Please install the Coq wrapper for this version of Rocq.";;
+        esac
         missingtools=true;;
 esac
 
diff --git a/coq b/coq
index 925bc4b9a1..8dee421abc 100755
--- a/coq
+++ b/coq
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Start coqide with the right options
+# Start rocqide/coqide with the right options
 # Use the Makefile to rebuild dependencies if needed
 # Recompile the modified file after coqide editing
 
@@ -10,4 +10,13 @@ make -q ${1}o || {
    done)
 }
 
-"${COQBIN}coqide" -async-proofs off $1 && make ${1}o
+if command -v "${COQBIN}rocqide" >/dev/null 2>&1; then
+  cmd="${COQBIN}rocqide"
+elif command -v "${COQBIN}coqide" >/dev/null 2>&1; then
+  cmd="${COQBIN}coqide"
+else
+  echo "Cannot find rocqide / coqide" >&2
+  exit 2
+fi
+
+"$cmd" -async-proofs off $1 && make ${1}o
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 514c6cbdfb..dc71de3e63 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -14,7 +14,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import BinPos.
+From Coq Require Import BinPos.
 
 (* OCaml's string type. *)
 Parameter string : Type.
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index 25213c7ed6..b234b0b34f 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -16,8 +16,8 @@
 
 %{
 
-Require Extraction.
-Require Import List.
+From Coq Require Extraction.
+From Coq Require Import List.
 Require Cabs.
 
 %}
diff --git a/driver/Compiler.v b/driver/Compiler.v
index b00d067e98..44791ac8f9 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -13,7 +13,7 @@
 (** The whole compiler and its proof of semantic preservation *)
 
 (** Libraries. *)
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Errors.
 Require Import AST Linking Smallstep.
 (** Languages (syntax and semantics). *)
diff --git a/driver/Complements.v b/driver/Complements.v
index 3660fff0cf..d3974c2f7c 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -12,7 +12,7 @@
 
 (** Corollaries of the main semantic preservation theorem. *)
 
-Require Import Classical.
+From Coq Require Import Classical.
 Require Import Coqlib Errors.
 Require Import AST Linking Events Smallstep Behaviors.
 Require Import Csyntax Csem Cstrategy Asm.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index a714c8313a..66f93fa185 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -14,31 +14,18 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Coqlib.
-Require Wfsimpl.
-Require DecidableClass Decidableplus.
-Require AST.
-Require Iteration.
-Require Floats.
-Require SelectLong.
-Require Selection.
-Require RTLgen.
-Require Inlining.
-Require ValueDomain.
-Require Tailcall.
-Require Allocation.
-Require Bounds.
-Require Ctypes.
-Require Csyntax.
-Require Ctyping.
-Require Clight.
+From Coq Require DecidableClass.
+Require Coqlib Wfsimpl Decidableplus Iteration.
+Require AST Floats.
+Require SelectLong Selection RTLgen Inlining ValueDomain.
+Require Tailcall Allocation Bounds.
+Require Ctypes Csyntax Ctyping Clight.
 Require Compiler.
 Require Parser.
 Require Initializers.
 
 (* Standard lib *)
-Require Import ExtrOcamlBasic.
-Require Import ExtrOcamlString.
+From Coq Require Import ExtrOcamlBasic ExtrOcamlString.
 
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
diff --git a/flocq/Calc/Bracket.v b/flocq/Calc/Bracket.v
index fe5a895d0b..4fcc5b2e60 100644
--- a/flocq/Calc/Bracket.v
+++ b/flocq/Calc/Bracket.v
@@ -651,7 +651,7 @@ now apply Zpower_gt_1.
 now apply Z_mod_lt.
 rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_IZR.
 rewrite Zmult_comm, Zplus_assoc.
-(try now rewrite <- Z_div_mod_eq_full); now rewrite <- Z_div_mod_eq.  (* remove the try and the second part when requiring Coq >= 8.14 *)
+now rewrite <- Z_div_mod_eq_full.
 Qed.
 
 Theorem inbetween_float_new_location_single :
diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v
index f412aa199f..917787db30 100644
--- a/flocq/Core/Digits.v
+++ b/flocq/Core/Digits.v
@@ -1119,11 +1119,15 @@ Theorem Zdigits_succ_le :
   forall x, (0 <= x)%Z ->
   (Zdigits (x + 1) <= Zdigits x + 1)%Z.
 Proof.
-  destruct x as [| p | p]; [intros _; now simpl | intros _ | lia].
-  transitivity (Zdigits (Z.pos p * beta ^ 1));
-    [apply Zdigits_le; [lia |] | rewrite Zdigits_mult_Zpower; lia].
-  apply Ztac.Zlt_le_add_1. rewrite <-Z.mul_1_r at 1. apply Zmult_lt_compat_l; [lia |].
-  rewrite Z.pow_1_r. apply radix_gt_1.
+  intros [|p|p]; try easy.
+  intros _.
+  rewrite <- Zdigits_mult_Zpower by easy.
+  apply Zdigits_le. easy.
+  apply Z.le_trans with (Z.pos p * 2)%Z.
+  lia.
+  apply Zmult_le_compat_l. 2: easy.
+  rewrite Z.pow_1_r.
+  apply (Zlt_le_succ 1), radix_gt_1.
 Qed.
 
 End Fcore_digits.
diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v
index 7d0c2268ef..82e65fbd6a 100644
--- a/flocq/Core/FLT.v
+++ b/flocq/Core/FLT.v
@@ -416,6 +416,23 @@ fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.
 rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia.
 Qed.
 
+Lemma pred_FLT_exact_shift :
+  forall x e,
+  (x <> 0)%R ->
+  (emin + prec + 1 <= mag beta x)%Z ->
+  (emin + prec - mag beta x + 1 <= e)%Z ->
+  (pred beta FLT_exp (x * bpow e) = pred beta FLT_exp x * bpow e)%R.
+Proof.
+intros x e Nzx Hmx He.
+unfold pred.
+rewrite Ropp_mult_distr_l.
+rewrite succ_FLT_exact_shift.
+apply Ropp_mult_distr_l.
+lra.
+now rewrite mag_opp.
+now rewrite mag_opp.
+Qed.
+
 Theorem ulp_FLT_pred_pos :
   forall x,
   generic_format beta FLT_exp x ->
diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v
index cb23982bb2..82e321649e 100644
--- a/flocq/Core/FLX.v
+++ b/flocq/Core/FLX.v
@@ -341,6 +341,16 @@ fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.
 rewrite ulp_FLX_exact_shift; ring.
 Qed.
 
+Lemma pred_FLX_exact_shift :
+  forall x e,
+  (pred beta FLX_exp (x * bpow e) = pred beta FLX_exp x * bpow e)%R.
+Proof.
+intros x e.
+unfold pred.
+rewrite Ropp_mult_distr_l, succ_FLX_exact_shift.
+apply Ropp_mult_distr_l.
+Qed.
+
 (** FLX is a nice format: it has a monotone exponent... *)
 Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
 Proof.
diff --git a/flocq/IEEE754/BinarySingleNaN.v b/flocq/IEEE754/BinarySingleNaN.v
index 32af023078..2c3e8b3513 100644
--- a/flocq/IEEE754/BinarySingleNaN.v
+++ b/flocq/IEEE754/BinarySingleNaN.v
@@ -70,6 +70,18 @@ Definition SF2B x :=
   | S754_nan => fun _ => B754_nan
   end.
 
+Definition SF2B' x :=
+  match x with
+  | S754_zero s => B754_zero s
+  | S754_infinity s => B754_infinity s
+  | S754_nan => B754_nan
+  | S754_finite s m e =>
+    match bounded m e as b return bounded m e = b -> _ with
+    | true => B754_finite s m e
+    | false => fun H => B754_nan
+    end eq_refl
+  end.
+
 Definition B2SF x :=
   match x with
   | B754_finite s m e _ => S754_finite s m e
@@ -234,6 +246,19 @@ intros Hx.
 apply f_equal, eqbool_irrelevance.
 Qed.
 
+Theorem SF2B'_B2SF :
+  forall x,
+  SF2B' (B2SF x) = x.
+Proof.
+intros [s|s| |s m e H] ; try easy.
+apply B2SF_inj.
+simpl.
+generalize (eq_refl (bounded m e)).
+pattern (bounded m e) at 2 3.
+apply eq_sym in H.
+now elim H.
+Qed.
+
 Definition is_finite_strict f :=
   match f with
   | B754_finite _ _ _ _ => true
@@ -886,6 +911,27 @@ destruct mrs as (m, r, s).
 now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
 Qed.
 
+Lemma shr_nat :
+  forall mrs e n, (0 <= n)%Z ->
+  shr mrs e n = (iter_nat shr_1 (Z.to_nat n) mrs, (e + n)%Z).
+Proof.
+intros mrs e n Hn.
+destruct n as [|n|n] ; simpl.
+now rewrite Zplus_0_r.
+now rewrite iter_pos_nat.
+easy.
+Qed.
+
+Lemma le_shr1_le :
+  forall mrs, (0 <= shr_m mrs)%Z ->
+  (0 <= shr_m (shr_1 mrs))%Z /\
+  (2 * shr_m (shr_1 mrs) <= shr_m mrs < 2 * (shr_m (shr_1 mrs) + 1))%Z.
+Proof.
+  intros [[|p|p] r s] ; try easy.
+  intros _.
+  destruct p as [p|p|] ; simpl ; lia.
+Qed.
+
 Theorem inbetween_shr :
   forall x m e l n,
   (0 <= m)%Z ->
@@ -893,70 +939,62 @@ Theorem inbetween_shr :
   let '(mrs, e') := shr (shr_record_of_loc m l) e n in
   inbetween_float radix2 (shr_m mrs) e' x (loc_of_shr_record mrs).
 Proof.
-intros x m e l n Hm Hl.
-destruct n as [|n|n].
-now destruct l as [|[| |]].
-2: now destruct l as [|[| |]].
-unfold shr.
-rewrite iter_pos_nat.
-rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
-induction (nat_of_P n).
-simpl.
-rewrite Zplus_0_r.
-now destruct l as [|[| |]].
-rewrite iter_nat_S.
-rewrite inj_S.
-unfold Z.succ.
-rewrite Zplus_assoc.
-revert IHn0.
-apply inbetween_shr_1.
-clear -Hm.
-induction n0.
-now destruct l as [|[| |]].
-rewrite iter_nat_S.
-revert IHn0.
-generalize (iter_nat shr_1 n0 (shr_record_of_loc m l)).
-clear.
-intros (m, r, s) Hm.
-now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
-Qed.
-
-Lemma le_shr1_le :
-  forall mrs, (0 <= shr_m mrs)%Z ->
-  (0 <= 2 * shr_m (shr_1 mrs) <= shr_m mrs)%Z /\
-  (shr_m mrs < 2 * (shr_m (shr_1 mrs) + 1))%Z.
-Proof.
-  destruct mrs as [m r s]. simpl.
-  destruct m as [| p | p]; [simpl; lia | intros _ | intros; easy].
-  destruct p; simpl; [| | lia].
-  - rewrite Pos2Z.inj_xO, Pos2Z.inj_xI. lia.
-  - rewrite Pos2Z.inj_xO. lia.
+  intros x m e l n Hm Hl.
+  destruct (Zle_or_lt 0 n).
+  2: {
+    destruct n as [|n|n] ; try easy.
+    simpl.
+    now rewrite shr_m_shr_record_of_loc, loc_of_shr_record_of_loc. }
+  rewrite shr_nat by easy.
+  rewrite <- (Z2Nat.id n) at 2 by easy.
+  clear H.
+  induction (Z.to_nat n) as [|n' IHn].
+  { rewrite Zplus_0_r.
+    simpl.
+    now rewrite shr_m_shr_record_of_loc, loc_of_shr_record_of_loc. }
+  rewrite iter_nat_S, inj_S.
+  unfold Z.succ.
+  rewrite Zplus_assoc.
+  revert IHn.
+  apply inbetween_shr_1.
+  clear -Hm.
+  induction n'.
+  simpl.
+  now rewrite shr_m_shr_record_of_loc.
+  rewrite iter_nat_S.
+  now apply le_shr1_le.
 Qed.
 
 Lemma le_shr_le :
   forall mrs e n,
   (0 <= shr_m mrs)%Z -> (0 <= n)%Z ->
-  (0 <= 2 ^ n * shr_m (fst (shr mrs e n)) <= shr_m mrs)%Z /\
-  (shr_m mrs < 2 ^ n * (shr_m (fst (shr mrs e n)) + 1))%Z.
-Proof.
-  intros mrs e n Hmrs.
-  destruct n as [| n | n ];
-    [intros _; simpl; now destruct (shr_m mrs); simpl; lia | intro Hn | lia].
-  unfold shr.
-  rewrite iter_pos_nat. rewrite <-!(positive_nat_Z n). simpl fst.
-  induction (nat_of_P n) as [| n' IHn']; [simpl; destruct (shr_m mrs); simpl; lia |].
-  rewrite !Nat2Z.inj_succ. rewrite Z.pow_succ_r; [| apply Zle_0_nat].
-
-  rewrite iter_nat_S. rewrite (Z.mul_comm 2%Z _), <-Z.mul_assoc.
-  destruct IHn' as [[IHn'1 IHn'2] IHn'3]. apply Z.mul_nonneg_cancel_l in IHn'1; [| lia].
-  repeat split;
-    [| transitivity (2 ^ Z.of_nat n' * shr_m (iter_nat shr_1 n' mrs))%Z; [| auto] |].
-  - apply Z.mul_nonneg_nonneg; [lia |]. now apply le_shr1_le.
-  - apply Z.mul_le_mono_nonneg_l; [lia |]. now apply le_shr1_le.
-  - apply Z.lt_le_trans with
-      (2 ^ Z.of_nat n' * (shr_m (iter_nat shr_1 n' mrs) + 1))%Z; [assumption |].
-    rewrite <-Z.mul_assoc. apply Z.mul_le_mono_nonneg_l; [lia |].
-    apply Ztac.Zlt_le_add_1. now apply le_shr1_le.
+  (0 <= shr_m (fst (shr mrs e n)))%Z /\
+  (2 ^ n * shr_m (fst (shr mrs e n)) <= shr_m mrs < 2 ^ n * (shr_m (fst (shr mrs e n)) + 1))%Z.
+Proof.
+  intros mrs e n Hmrs Hn.
+  rewrite shr_nat by easy.
+  simpl.
+  rewrite <- (Z2Nat.id n) at 2 4 by easy.
+  induction (Z.to_nat n) as [|n' IHn].
+  { simpl Z.pow. rewrite 2!Zmult_1_l.
+    simpl. lia. }
+  clear n Hn.
+  rewrite Nat2Z.inj_succ, Z.pow_succ_r by apply Zle_0_nat.
+  rewrite iter_nat_S.
+  revert IHn.
+  generalize (iter_nat shr_1 n' mrs).
+  intros mrs' [H [IH1 IH2]].
+  destruct (le_shr1_le _ H) as [H' [K1 K2]].
+  apply (conj H').
+  rewrite (Zmult_comm 2), <- 2!Zmult_assoc.
+  split.
+  - apply Z.le_trans with (2 := IH1).
+    apply Zmult_le_compat_l with (1 := K1).
+    apply (Zpower_ge_0 radix2).
+  - apply Z.lt_le_trans with (1 := IH2).
+    apply Zmult_le_compat_l.
+    lia.
+    apply (Zpower_ge_0 radix2).
 Qed.
 
 Lemma shr_limit :
@@ -979,12 +1017,12 @@ Proof.
       destruct mrs as [m r s]. simpl in Hmrs00, Hmrs01, Hmrs1. rewrite Hmrs00.
       simpl. now rewrite Hmrs01.
     + intros mrs Hmrs0 Hmrs1. simpl iter_nat.
-      destruct (le_shr1_le mrs) as [[Hmrs'0 Hmrs'1] Hmrs'2]; [destruct Hmrs0; lia |].
+      destruct (le_shr1_le mrs) as [Hmrs'0 [Hmrs'1 Hmrs'2]]; [destruct Hmrs0; lia |].
       set (mrs' := shr_1 mrs). apply IHn''.
       * case (0 <? shr_m (shr_1 mrs))%Z eqn:Hmrs'3;
          [apply Zlt_is_lt_bool in Hmrs'3; now left |].
         fold mrs' in Hmrs'0, Hmrs'1, Hmrs'2, Hmrs'3.
-        apply Z.ltb_ge in Hmrs'3. apply Z.mul_nonneg_cancel_l in Hmrs'0; [| easy].
+        apply Z.ltb_ge in Hmrs'3.
         apply (Z.le_antisymm _ _ Hmrs'3) in Hmrs'0. right. split; [assumption |].
         destruct Hmrs0 as [Hmrs0 | [Hmrs00 Hmrs01]].
         -- rewrite Hmrs'0 in Hmrs'2. simpl in Hmrs'2.
@@ -1595,6 +1633,7 @@ destruct (ex' - ex)%Z as [|d|d] eqn:Hd ; simpl.
 - now replace ex with ex' by lia.
 - exfalso ; lia.
 - refine (conj _ eq_refl).
+  fold (shift_pos d mx).
   rewrite shift_pos_correct, Zmult_comm.
   change (Zpower_pos 2 d) with (Zpower radix2 (Z.opp (Z.neg d))).
   rewrite <- Hd.
@@ -2517,10 +2556,6 @@ Proof.
   (* N.B.: The hypothesis (ex < 0)%Z is only here to make the proof simpler. *)
   { intros Hex.
     rewrite mrs'_simpl.
-    apply (Z.mul_le_mono_pos_l _ _ (2 ^ (- ex))).
-    apply (Zpower_gt_0 radix2).
-    lia.
-    rewrite Z.mul_0_r.
     apply le_shr_le.
     easy.
     lia. }
@@ -2534,7 +2569,6 @@ Proof.
     unfold bounded, canonical_mantissa.
     assert (A : (fexp (Z.pos (digits2_pos p) + 0) <= 0)%Z).
     { rewrite Z.add_0_r in *. rewrite Zpos_digits2_pos in *.
-      destruct (le_shr_le mrs' ex (- ex)) as [H2 H3]; [now apply mrs'_ge_0 | lia |].
       destruct (le_choice_mode_le md sx (shr_m mrs') (loc_of_shr_record mrs')) as [H4 H5].
       rewrite H0 in H4, H5.
       transitivity (fexp (Zdigits radix2 (shr_m mrs' + 1)));
@@ -2677,13 +2711,11 @@ Proof.
       destruct (le_choice_mode_le mode_ZR sx (shr_m mrs') (loc_of_shr_record mrs')) as [H3 _].
       rewrite H2 in H3. unfold mrs' in H3. case (ex <? - prec)%Z in H3.
       * simpl in H3. lia.
-      * destruct (le_shr_le ({| shr_m := Z.pos mx; shr_r := false; shr_s := false |})
-          ex (- ex)) as [[H4 _] _]; [simpl; lia | lia |].
-        elim (Zle_not_lt 0 (Z.neg p)). 2: easy.
+      * elim (Zle_not_lt 0 (Z.neg p)). 2: easy.
         apply Z.le_trans with (2 := H3).
-        apply Zmult_le_0_reg_r with (2 ^ (- ex))%Z.
-        apply Z.lt_gt, (Zpower_gt_0 radix2). lia.
-        now rewrite Zmult_comm.
+        apply le_shr_le.
+        easy.
+        lia.
 Qed.
 
 (** A few values *)
@@ -3761,6 +3793,7 @@ Arguments B754_nan {prec} {emax}.
 Arguments B754_finite {prec} {emax}.
 
 Arguments SF2B {prec} {emax}.
+Arguments SF2B' {prec} {emax}.
 Arguments B2SF {prec} {emax}.
 Arguments B2R {prec} {emax}.
 
diff --git a/flocq/Version.v b/flocq/Version.v
index 17fc9d4bfd..fb6dee1344 100644
--- a/flocq/Version.v
+++ b/flocq/Version.v
@@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in
       parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | EmptyString => (major * 100 + minor)%N
     end in
-  parse "4.1.4"%string N0 N0.
+  parse "4.2.1"%string N0 N0.
diff --git a/lib/Axioms.v b/lib/Axioms.v
index d7b3d03629..f6baba3b30 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.v
@@ -16,8 +16,7 @@
 
 (** This file collects some axioms used throughout the CompCert development. *)
 
-Require ClassicalFacts.
-Require FunctionalExtensionality.
+From Coq Require ClassicalFacts FunctionalExtensionality.
 
 (** * Extensionality axioms *)
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 39b76a3947..56de5ae4ac 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -18,12 +18,7 @@
     used throughout the development.  It complements the Coq standard
     library. *)
 
-Require Export String.
-Require Export ZArith.
-Require Export Znumtheory.
-Require Export List.
-Require Export Bool.
-Require Export Lia.
+From Coq Require Export String ZArith Znumtheory List Bool Lia.
 
 (** * Useful tactics *)
 
@@ -1338,7 +1333,7 @@ End DECIDABLE_PREDICATE.
 
 (** * Well-founded orderings *)
 
-Require Import Relations.
+From Coq Require Import Relations.
 
 (** A non-dependent version of lexicographic ordering. *)
 
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 224c9640fe..222e6b6d3f 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.v
@@ -20,7 +20,7 @@
   of Coq 8.5 with more instances of decidable properties, including
   universal and existential quantification over finite types. *)
 
-Require Export DecidableClass.
+From Coq Require Export DecidableClass.
 Require Import Coqlib.
 
 Ltac decide_goal := eapply Decidable_sound; reflexivity.
diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
index 936814c185..c632052797 100644
--- a/lib/FSetAVLplus.v
+++ b/lib/FSetAVLplus.v
@@ -18,8 +18,8 @@
   with extra interval-based operations, more efficient than standard
   operations. *)
 
-Require Import FSetInterface.
-Require FSetAVL.
+From Coq Require Import FSetInterface.
+From Coq Require FSetAVL.
 Require Import Coqlib.
 
 Module Make(X: OrderedType).
diff --git a/lib/Floats.v b/lib/Floats.v
index ff2584871b..476074217e 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -17,11 +17,10 @@
 
 (** Formalization of floating-point numbers, using the Flocq library. *)
 
-Require Import Reals.
+From Coq Require Import Reals Program.
 Require Import Coqlib Zbits Integers.
 From Flocq Require Import BinarySingleNaN Binary Bits Core.
 Require Import IEEE754_extra.
-Require Import Program.
 Require Archi.
 Import ListNotations.
 
diff --git a/lib/Heaps.v b/lib/Heaps.v
index def9da9742..ffe90ef7a6 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -22,10 +22,8 @@
     (If an element is already in a heap, inserting it again does nothing.)
 *)
 
-Require Import FunInd.
-Require Import Coqlib.
-Require Import FSets.
-Require Import Ordered.
+From Coq Require Import FunInd FSets.
+Require Import Coqlib Ordered.
 
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index f7c2487b93..b63884fdf3 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -18,14 +18,9 @@
 (** Additional operations and proofs about IEEE-754 binary
     floating-point numbers, on top of the Flocq library. *)
 
-Require Import Reals.
-Require Import SpecFloat.
+From Coq Require Import Reals SpecFloat ZArith Psatz Bool Eqdep_dec.
 From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
                           BinarySingleNaN Binary Round_odd.
-Require Import ZArith.
-Require Import Psatz.
-Require Import Bool.
-Require Import Eqdep_dec.
 
 Local Open Scope Z_scope.
 
diff --git a/lib/Integers.v b/lib/Integers.v
index a0f1329ed3..38b65c6475 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -16,7 +16,7 @@
 
 (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *)
 
-Require Import Eqdep_dec Zquot Zwf.
+From Coq Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits.
 Require Archi.
 
diff --git a/lib/Intv.v b/lib/Intv.v
index d5d024aa69..9be0759fd4 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -16,10 +16,8 @@
 
 (** Definitions and theorems about semi-open integer intervals *)
 
+From Coq Require Import Zwf Program.Wf Recdef.
 Require Import Coqlib.
-Require Import Zwf.
-Require Coq.Program.Wf.
-Require Import Recdef.
 
 Definition interv : Type := (Z * Z)%type.
 
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 5067206948..7b5236bc8f 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -202,8 +202,7 @@ End PrimIter.
   [None] means that iteration does not terminate.
   [Some b] means that iteration terminates with the result [b]. *)
 
-Require Import Classical.
-Require Import ClassicalDescription.
+From Coq Require Import Classical ClassicalDescription.
 
 Module GenIter.
 
diff --git a/lib/Lattice.v b/lib/Lattice.v
index aea331a0cf..6431ad9915 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -17,9 +17,8 @@
 
 (** Constructions of semi-lattices. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import FSets.
+From Coq Require Import FSets.
+Require Import Coqlib Maps.
 
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.
diff --git a/lib/Maps.v b/lib/Maps.v
index 066d80521a..b85b653b52 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1554,7 +1554,7 @@ Module ZTree := ITree(ZIndexed).
 
 (** * Additional properties over trees *)
 
-Require Import Equivalence EquivDec.
+From Coq Require Import Equivalence EquivDec.
 
 Module Tree_Properties(T: TREE).
 
diff --git a/lib/Ordered.v b/lib/Ordered.v
index d02892cee7..c22c47097f 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -17,10 +17,8 @@
 (** Constructions of ordered types, for use with the [FSet] functors
   for finite sets and the [FMap] functors for finite maps. *)
 
-Require Import FSets.
-Require Import Coqlib.
-Require Import Maps.
-Require Import Integers.
+From Coq Require Import FSets.
+Require Import Coqlib Maps Integers.
 
 Create HintDb ordered_type.
 
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 269d3a594e..6db299f625 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -2,8 +2,8 @@
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
-(*      Laurence Rideau, INRIA Sophia-Antipolis-M\u00e9diterran\u00e9e           *)
-(*      Bernard Paul Serpette, INRIA Sophia-Antipolis-M\u00e9diterran\u00e9e     *)
+(*      Laurence Rideau, INRIA Sophia-Antipolis-Méditerranée           *)
+(*      Bernard Paul Serpette, INRIA Sophia-Antipolis-Méditerranée     *)
 (*      Xavier Leroy, INRIA Paris-Rocquencourt                         *)
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
@@ -53,10 +53,8 @@
   #</A>#
 *)
 
-Require Import Relations.
-Require Import Axioms.
-Require Import Coqlib.
-Require Import Recdef.
+From Coq Require Import Relations Recdef.
+Require Import Axioms Coqlib.
 
 Section PARMOV.
 
diff --git a/lib/Postorder.v b/lib/Postorder.v
index 0be7d0b455..5a8a6a6953 100644
--- a/lib/Postorder.v
+++ b/lib/Postorder.v
@@ -16,12 +16,8 @@
 
 (** Postorder numbering of a directed graph. *)
 
-Require Import Wellfounded.
-Require Import Permutation.
-Require Import Mergesort.
-Require Import Coqlib.
-Require Import Maps.
-Require Import Iteration.
+From Coq Require Import Wellfounded Permutation Mergesort.
+Require Import Coqlib Maps Iteration.
 
 (** The graph is presented as a finite map from nodes (of type [positive])
   to the lists of their successors. *)
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 1bc2f657f9..abd73729d7 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -16,7 +16,7 @@
 
 (** A persistent union-find data structure. *)
 
-Require Coq.Program.Wf.
+From Coq Require Program.Wf.
 Require Import Coqlib.
 
 Open Scope nat_scope.
diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v
index 6e52cd3613..75d4ba8009 100644
--- a/lib/Wfsimpl.v
+++ b/lib/Wfsimpl.v
@@ -18,9 +18,8 @@
   interface to the [Wf] module of Coq's standard library, where the functions
   to be defined have non-dependent types, and function extensionality is assumed. *)
 
+From Coq Require Import Wf_nat.
 Require Import Axioms.
-Require Import Init.Wf.
-Require Import Wf_nat.
 
 Set Implicit Arguments.
 
diff --git a/lib/Zbits.v b/lib/Zbits.v
index 2d82139aab..6470912c79 100644
--- a/lib/Zbits.v
+++ b/lib/Zbits.v
@@ -17,7 +17,7 @@
 (** Additional operations and proofs about binary integers,
     on top of the ZArith standard library. *)
 
-Require Import Psatz Zquot.
+From Coq Require Import Psatz Zquot.
 Require Import Coqlib.
 
 (** ** Modulo arithmetic *)
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 9dede4c73d..5bb4cfe776 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for PowerPC *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := false.
 
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index c9cef3046d..3bfdaacd1f 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.v
@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 Local Open Scope asttyp_scope.
 
diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v
index 68eb42e711..319f323eae 100644
--- a/powerpc/CombineOpproof.v
+++ b/powerpc/CombineOpproof.v
@@ -13,15 +13,9 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
-Require Import FunInd.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+From Coq Require Import FunInd.
+Require Import Coqlib AST Integers Values Memory.
+Require Import Op Registers RTL.
 Require Import CSEdomain.
 Require Import CombineOp.
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index eeca880a7f..373433623f 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -10,12 +10,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
+From Coq Require Import String.
+Require Import Coqlib Decidableplus Maps.
+Require Import AST Op.
 
 (** ** Machine registers *)
 
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index ea14668f17..bee9dfc93b 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -12,7 +12,8 @@
 
 (** Correctness of instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Zbits Integers Floats Errors.
+From Coq Require Import String.
+Require Import Coqlib Maps Zbits Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
diff --git a/riscV/Archi.v b/riscV/Archi.v
index e33c3e841c..ce93572870 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for RISC-V *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Parameter ptr64 : bool.
 
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 1996f6a1a5..7ef2fb64af 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.v
@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type := .
diff --git a/riscV/CombineOpproof.v b/riscV/CombineOpproof.v
index 81226a8201..22e2b8c047 100644
--- a/riscV/CombineOpproof.v
+++ b/riscV/CombineOpproof.v
@@ -13,15 +13,9 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
-Require Import FunInd.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+From Coq Require Import FunInd.
+Require Import Coqlib AST Integers Values Memory.
+Require Import Op Registers RTL.
 Require Import CSEdomain.
 Require Import CombineOp.
 
diff --git a/riscV/Machregs.v b/riscV/Machregs.v
index 89fa37b025..7299ccd8ac 100644
--- a/riscV/Machregs.v
+++ b/riscV/Machregs.v
@@ -15,13 +15,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
+From Coq Require Import String.
+Require Import Coqlib Decidableplus Maps.
+Require Import AST Integers Op.
 
 (** ** Machine registers *)
 
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v
index 3794e05035..97d050bb31 100644
--- a/riscV/SelectLongproof.v
+++ b/riscV/SelectLongproof.v
@@ -17,7 +17,8 @@
 
 (** Correctness of instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Integers Floats Errors.
+From Coq Require Import String.
+Require Import Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
diff --git a/test b/test
index 02b559f624..72ca254ccd 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 02b559f624ff271053998b892ec6de8cf4e7a36e
+Subproject commit 72ca254ccd357849215b596610807bfc3ec2d807
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index 3244f38c55..aeb3deb5ec 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.v
@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 Local Open Scope asttyp_scope.
 
diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v
index 1712538eb1..5839f78056 100644
--- a/x86/CombineOpproof.v
+++ b/x86/CombineOpproof.v
@@ -13,7 +13,7 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib.
 Require Import Integers Values Memory.
 Require Import Op RTL CSEdomain.
diff --git a/x86/Machregs.v b/x86/Machregs.v
index 6c8fb82975..20cc8db745 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -10,13 +10,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
+From Coq Require Import String.
+Require Import Coqlib Decidableplus Maps.
+Require Import AST Integers Op.
 
 (** ** Machine registers *)
 
diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v
index 3bef632d82..5f79b7aa4a 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -12,7 +12,8 @@
 
 (** Correctness of instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Integers Floats Errors.
+From Coq Require Import String.
+Require Import Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index 775bdd4419..14c97e2b4a 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for x86 in 32-bit mode *)
 
+From Coq Require Import List ZArith.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := false.
 
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 9df30c8855..50cb16918c 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for x86 in 64-bit mode *)
 
+From Coq Require Import List ZArith.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := true.