Merge pull request #148 from proux01/stdlib_repo

Adapt to coq/coq#19530
jwiegley · Sep 17, 2024 · b1033ae · b1033ae
2 parents 268c570 + 04da82e
commit b1033ae
Show file tree

Hide file tree

Showing 7 changed files with 15 additions and 17 deletions.
diff --git a/Instance/Lambda/Ltac.v b/Instance/Lambda/Ltac.v
@@ -1,5 +1,5 @@
-Require Import Coq.Unicode.Utf8.
-Require Import Coq.Program.Program.
+From Coq Require Import Utf8.
+From Coq Require Import Program.
 
 Local Set Warnings "-deprecated-notation".
 

diff --git a/Lib/Foundation.v b/Lib/Foundation.v
@@ -1,5 +1,5 @@
-Require Export Coq.Program.Program.
-Require Export Coq.Classes.CMorphisms.
+From Coq Require Export Program.
+From Coq Require Export CMorphisms.
 
 Generalizable All Variables.
 Set Primitive Projections.

diff --git a/Lib/MapDecide.v b/Lib/MapDecide.v
@@ -1,6 +1,6 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.FSets.FMaps.
-Require Import Coq.micromega.Lia.
+From Coq Require Import NArith.
+From Coq Require Import FMaps.
+From Coq Require Import Lia.
 
 (* Override ++> notation with the crelation-based version. *)
 #[local] Set Warnings "-notation-overridden".

diff --git a/Theory/Coq/List.v b/Theory/Coq/List.v
@@ -399,9 +399,7 @@ Instance List_Applicative : Applicative list := {
   ap   := @list_ap
 }.
 
-Require Import
-  Coq.Relations.Relations
-  Coq.Reals.ROrderedType.
+From Coq Require Import Relations ROrderedType.
 
 Require Export Coq.Lists.List.
 

diff --git a/Theory/Coq/Map.v b/Theory/Coq/Map.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.micromega.Lia.
+From Coq Require Import List.
+From Coq Require Import Lia.
 
 From Equations Require Import Equations.
 Set Equations With UIP.

diff --git a/Theory/Metacategory.v b/Theory/Metacategory.v
@@ -1,7 +1,7 @@
-Require Import Coq.Structures.DecidableTypeEx.
-Require Import Coq.FSets.FMapFacts.
+From Coq Require Import DecidableTypeEx.
+From Coq Require Import FMapFacts.
 Require Import Category.Lib.FMapExt.
-Require Import Coq.Arith.PeanoNat.
+From Coq Require Import PeanoNat.
 
 (* Override ++> notation with the crelation-based version. *)
 #[local] Set Warnings "-notation-overridden".

diff --git a/Theory/Metacategory/ArrowsOnly.v b/Theory/Metacategory/ArrowsOnly.v
@@ -1,5 +1,5 @@
-Require Import Coq.NArith.NArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import NArith.
+From Coq Require Import Lia.
 
 Require Import Category.Lib.
 Require Import Category.Lib.MapDecide.