Add From Coq to Require of standard library modules

Rocq 9.0 wants `From Stdlib`, but Coq 8 understands `From Coq`.
Changing `From Coq` to `From Stdlib` later will be easy.

Author: xavierleroy

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.
 

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.
 

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.

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 := .

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.

aarch64/Machregs.v

@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Decidableplus Maps.
 Require Import AST Op.
 

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.
 

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 := .

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.
 

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 *)
 

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.

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.

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.

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.

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.
 

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.

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.

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.
 

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.

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 *)

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.

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.
 

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.

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.

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.

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.

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.

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.

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.

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.
 

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.

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.

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.

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.

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.

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.