Adapt to rocq-prover/rocq#21851 (#129)

* Adapt to rocq-prover/rocq#21851

* Update CI

9.2.0 was released last week but we don't have the docker image yet.

Author: proux01

.github/workflows/coq.yml

@@ -11,7 +11,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ "dev" , "9.0" , "8.20" , "8.19" ]
+        coq-version: [ "dev" , "9.1" , "9.0" ]
         targets: [ "fiat-core parsers parsers-examples coq-ci" ]
 
     name: ${{ matrix.coq-version }} (${{ matrix.targets }})

Bedrock/Nomega.v

@@ -1,7 +1,7 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (* Make [omega] work for [N] *)
 
-Require Import Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith.
+Require Import Stdlib.Arith.Arith Stdlib.ZArith.ZArith Stdlib.NArith.NArith.
 
 Local Open Scope N_scope.
 

Bedrock/Word.v

@@ -1,7 +1,7 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** Fixed precision machine words *)
 
-Require Import Coq.Arith.Arith
+Require Import Stdlib.Arith.Arith
         Coq.NArith.NArith
         Coq.Bool.Bool
         Coq.ZArith.ZArith.
@@ -283,7 +283,7 @@ Qed.
 
 Hint Resolve shatter_word_0.
 
-Require Import Coq.Logic.Eqdep_dec.
+Require Import Stdlib.Logic.Eqdep_dec.
 
 Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}.
   refine (fix weq sz (x : word sz) : forall y : word sz, {x = y} + {x <> y} :=
@@ -369,7 +369,7 @@ Theorem split2_combine : forall sz1 sz2 (w : word sz1) (z : word sz2),
   induction sz1; shatterer.
 Qed.
 
-Require Import Coq.Logic.Eqdep_dec.
+Require Import Stdlib.Logic.Eqdep_dec.
 
 
 Theorem combine_assoc : forall n1 (w1 : word n1) n2 n3 (w2 : word n2) (w3 : word n3) Heq,

src/ADT/ADTHide.v

@@ -1,4 +1,5 @@
-Require Import Fiat.Common Fiat.Computation.Core Fiat.ADT.Core Coq.Sets.Ensembles.
+Require Import Fiat.Common Fiat.Computation.Core Fiat.ADT.Core.
+From Stdlib Require Import Ensembles.
 
 Section HideADT.
 

src/ADT/ComputationalADT.v

@@ -1,5 +1,5 @@
 Require Export Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.
-Require Import Coq.Sets.Ensembles.
+From Stdlib Require Import Ensembles.
 
 Generalizable All Variables.
 Set Implicit Arguments.

src/ADT/Core.v

@@ -1,5 +1,5 @@
 Require Export Fiat.Common Fiat.Computation Fiat.ADT.ADTSig.
-Require Import Coq.Sets.Ensembles.
+From Stdlib Require Import Ensembles.
 
 Generalizable All Variables.
 Set Implicit Arguments.

src/ADTInduction.v

@@ -1,7 +1,7 @@
 Require Import Fiat.ADT Fiat.ADTNotation.
 
-Require Import Coq.Sets.Ensembles.
-Require Import Coq.Lists.List.
+From Stdlib Require Import Ensembles.
+From Stdlib Require Import List.
 
 Import ListNotations.
 

src/ADTNotation/BuildADT.v

@@ -1,7 +1,5 @@
-Require Import Coq.Sets.Ensembles
-        Coq.Lists.List
-        Coq.Strings.String
-        Fiat.Common
+From Stdlib Require Import Ensembles List String.
+Require Import Fiat.Common
         Fiat.Computation
         Fiat.ADT.ADTSig
         Fiat.ADT.Core

src/ADTNotation/BuildADTReplaceMethods.v

@@ -1,6 +1,5 @@
-Require Import Coq.Lists.List
-        Coq.Strings.String
-        Fiat.ADT.ADTSig
+From Stdlib Require Import List String.
+Require Import Fiat.ADT.ADTSig
         Fiat.ADT.Core
         Fiat.Common
         Fiat.Common.BoundedLookup

src/ADTNotation/BuildADTSig.v

@@ -1,5 +1,5 @@
 Require Import Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADT.ADTSig.
-Require Import Coq.Lists.List Coq.Strings.String.
+From Stdlib Require Import List String.
 
 (* Notation for ADT Signatures. *)
 
@@ -102,7 +102,7 @@ Delimit Scope ADTSig_scope with ADTSig.
 
 (* Notation for ADT signatures utilizing [BuildADTSig]. *)
 
-Require Import Coq.Vectors.Vector.
+From Stdlib Require Import Vector.
 Import Vectors.Vector.VectorNotations.
 
 Delimit Scope vector_scope with vector.