mit-plv · JasonGross · Apr 2, 2026 · Apr 1, 2026 · Apr 2, 2026
diff --git a/.github/workflows/coq.yml b/.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 }})

diff --git a/Bedrock/Nomega.v b/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.
 

diff --git a/Bedrock/Word.v b/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,

diff --git a/src/ADT/ADTHide.v b/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.
 

diff --git a/src/ADT/ComputationalADT.v b/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.

diff --git a/src/ADT/Core.v b/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.

diff --git a/src/ADTInduction.v b/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.
 

diff --git a/src/ADTNotation/BuildADT.v b/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

diff --git a/src/ADTNotation/BuildADTReplaceMethods.v b/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

diff --git a/src/ADTNotation/BuildADTSig.v b/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.

diff --git a/src/ADTNotation/BuildComputationalADT.v b/src/ADTNotation/BuildComputationalADT.v
@@ -1,8 +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

diff --git a/src/ADTRefinement/BuildADTRefinements/AddCache.v b/src/ADTRefinement/BuildADTRefinements/AddCache.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Fiat.Common
+Require Import Stdlib.Lists.List Fiat.Common
         Fiat.ADT.ADTSig Fiat.ADT.Core
         Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT
         Fiat.Common.ilist Fiat.Common.BoundedLookup

diff --git a/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v b/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Fiat.Common
+Require Import Stdlib.Lists.List Fiat.Common
         Fiat.Common.ilist
         Fiat.Common.BoundedLookup
         Fiat.Common.IterateBoundedIndex

diff --git a/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v b/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Fiat.Common
+Require Import Stdlib.Lists.List Fiat.Common
         Fiat.Common.ilist
         Fiat.Common.BoundedLookup
         Fiat.Common.IterateBoundedIndex

diff --git a/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v b/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Fiat.Common
+Require Import Stdlib.Lists.List Fiat.Common
         Fiat.ADT.ADTSig Fiat.ADT.Core
         Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT
         Fiat.Common.ilist Fiat.Common.BoundedLookup

diff --git a/src/ADTRefinement/Core.v b/src/ADTRefinement/Core.v
@@ -1,4 +1,5 @@
-Require Import Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles.
+Require Import Fiat.Common Fiat.Computation Fiat.ADT.
+From Stdlib Require Import Ensembles.
 
 Generalizable All Variables.
 Set Implicit Arguments.

diff --git a/src/ADTRefinement/FixedPoint.v b/src/ADTRefinement/FixedPoint.v
@@ -1,8 +1,8 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Fiat.ADT Fiat.ADTNotation.
 Require Export Fiat.Computation.FixComp.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Arith.PeanoNat.
+From Stdlib Require Import ZArith.
+Require Import Stdlib.Arith.PeanoNat.
 
 Import LeastFixedPointFun.
 

diff --git a/src/ADTRefinement/GeneralBuildADTRefinements.v b/src/ADTRefinement/GeneralBuildADTRefinements.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List Coq.Arith.Arith
-        Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core
+From Stdlib Require Import List Arith.
+Require Import Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core
         Fiat.ADT.ComputationalADT
         Fiat.Common.BoundedLookup
         Fiat.Common.ilist
@@ -16,7 +16,7 @@ Require Import Coq.Lists.List Coq.Arith.Arith
 
 Section BuildADTRefinements.
 
-  Require Import Coq.Strings.String.
+  From Stdlib Require Import String.
   Local Hint Resolve string_dec.
 
   Lemma refineADT_BuildADT_ReplaceConstructor

diff --git a/src/ADTRefinement/GeneralBuildADTTactics.v b/src/ADTRefinement/GeneralBuildADTTactics.v
@@ -1,6 +1,6 @@
 Require Export Fiat.ADTRefinement.GeneralBuildADTRefinements.
 (* TODO: Clean out these imports. *)
-Require Import Coq.Lists.List Coq.Arith.Arith
+Require Import Stdlib.Lists.List Stdlib.Arith.Arith
         Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core
         Fiat.ADT.ComputationalADT
         Fiat.Common.BoundedLookup

diff --git a/src/ADTRefinement/GeneralRefinements.v b/src/ADTRefinement/GeneralRefinements.v
@@ -1,6 +1,5 @@
-Require Import Coq.Lists.List
-        Coq.Strings.String
-        Fiat.Common
+From Stdlib Require Import List String.
+Require Import Fiat.Common
         Fiat.Common.ilist
         Fiat.Common.BoundedLookup
         Fiat.ADT.Core

diff --git a/src/ADTRefinement/Refinements/ADTCache.v b/src/ADTRefinement/Refinements/ADTCache.v
@@ -1,4 +1,4 @@
-Require Import Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv.
+Require Import Fiat.Common Fiat.Computation Fiat.ADT Stdlib.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv.
 
 Generalizable All Variables.
 Set Implicit Arguments.

diff --git a/src/ADTRefinement/Refinements/ADTRepInv.v b/src/ADTRefinement/Refinements/ADTRepInv.v
@@ -1,4 +1,4 @@
-Require Import Fiat.Common Fiat.Computation Coq.Sets.Ensembles
+Require Import Fiat.Common Fiat.Computation Stdlib.Sets.Ensembles
         Fiat.ADT.ADTSig Fiat.ADT.Core
         Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms
         Fiat.ADTRefinement.GeneralRefinements.

diff --git a/src/ADTRefinement/SetoidMorphisms.v b/src/ADTRefinement/SetoidMorphisms.v
@@ -1,4 +1,5 @@
-Require Import Fiat.Common Fiat.Computation Coq.Sets.Ensembles.
+Require Import Fiat.Common Fiat.Computation.
+From Stdlib Require Import Ensembles.
 Require Import Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core.
 
 (** Definitions for integrating [refineADT] into the setoid rewriting

diff --git a/src/CertifiedExtraction/Benchmarks/DNS.v b/src/CertifiedExtraction/Benchmarks/DNS.v
@@ -6,7 +6,7 @@ Require Import
 
 Opaque Transformer.transform_id.
 Opaque EncodeAndPad. (* FIXME move *)
-Require Import Coq.Program.Program.
+From Stdlib Require Import Program.
 
 Definition PacketAsCollectionOfVariables
            {av} vid vmask vquestion vanswer vauthority vadditional (p: packet_t)

diff --git a/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v b/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v
@@ -12,7 +12,7 @@ Require Export
         Fiat.CertifiedExtraction.Extraction.BinEncoders.BinEncoders.
 
 Require Import
-        Coq.Strings.String
+        Stdlib.Strings.String
         Coq.Vectors.Vector.
 
 Require Export

diff --git a/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v b/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v
@@ -1,4 +1,4 @@
-Require Import Coq.Strings.String.
+From Stdlib Require Import String.
 Require Import Bedrock.Platform.Facade.DFacade.
 Require Import Bedrock.Platform.Cito.SyntaxExpr.
 

diff --git a/src/CertifiedExtraction/Core.v b/src/CertifiedExtraction/Core.v
@@ -1,4 +1,4 @@
-Require Export Coq.Strings.String.
+Require Export Stdlib.Strings.String.
 Require Export Computation.Core ADTRefinement.
 Require Export Bedrock.Platform.Facade.DFacade Bedrock.Platform.Cito.StringMap.
 

diff --git a/src/CertifiedExtraction/CoreLemmas.v b/src/CertifiedExtraction/CoreLemmas.v
@@ -4,7 +4,7 @@ Require Export
         CertifiedExtraction.Utils
         CertifiedExtraction.StringMapUtils.
 
-Require Export Coq.Setoids.Setoid.
+Require Export Stdlib.Setoids.Setoid.
 
 Local Open Scope map_scope.
 Local Open Scope telescope_scope.

diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v b/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v
@@ -1,4 +1,4 @@
-Require Export Coq.NArith.NArith.
+Require Export Stdlib.NArith.NArith.
 
 Require Export Bedrock.Memory Bedrock.Word.
 Require Export

diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v b/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v
@@ -7,7 +7,7 @@ Require Export
         Fiat.CertifiedExtraction.Extraction.BinEncoders.RewriteRules.
 Unset Implicit Arguments.
 
-Require Import Coq.Lists.List.
+From Stdlib Require Import List.
 
 Ltac _compile_decide_padding_0 :=
   repeat first [ reflexivity |

diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v b/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v
@@ -23,7 +23,7 @@ Proof.
   destruct (encode1 _); simpl; destruct (encode2 _); reflexivity.
 Qed.
 
-Require Import Coq.Lists.List.
+From Stdlib Require Import List.
 Require Import Bedrock.Word.
 
 Theorem exist_irrel : forall A (P : A -> Prop) x1 pf1 x2 pf2,

diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v b/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v
@@ -1,4 +1,4 @@
-Require Import Coq.Program.Program.
+From Stdlib Require Import Program.
 
 Require Import
         Fiat.CertifiedExtraction.Core

diff --git a/src/CertifiedExtraction/Extraction/Core.v b/src/CertifiedExtraction/Extraction/Core.v
@@ -10,7 +10,7 @@ Require Export
         CertifiedExtraction.Extraction.Gensym
         CertifiedExtraction.Extraction.PreconditionSets.
 
-Require Import Coq.Strings.String.
+From Stdlib Require Import String.
 Global Open Scope string_scope.
 
 Ltac av_from_ext ext :=

diff --git a/src/CertifiedExtraction/Extraction/External/ScalarMethods.v b/src/CertifiedExtraction/Extraction/External/ScalarMethods.v
@@ -2,7 +2,7 @@ Require Import
         CertifiedExtraction.Extraction.External.Core
         CertifiedExtraction.Extraction.External.GenericMethods.
 
-Require Import Coq.Lists.List.
+From Stdlib Require Import List.
 
 Lemma CompileCallFacadeImplementationWW:
   forall {av} {env} fWW,

diff --git a/src/CertifiedExtraction/Extraction/Extraction.v b/src/CertifiedExtraction/Extraction/Extraction.v
@@ -1,5 +1,5 @@
 Require Export
-        Coq.Strings.String
+        Stdlib.Strings.String
         CertifiedExtraction.FacadeNotations
         CertifiedExtraction.Extraction.External.External.
 Require Import

diff --git a/src/CertifiedExtraction/Extraction/Gensym.v b/src/CertifiedExtraction/Extraction/Gensym.v
@@ -1,6 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
-Require Import Coq.Numbers.Natural.Peano.NPeano
-        Coq.Strings.String
+Require Import Stdlib.Numbers.Natural.Peano.NPeano
+        Stdlib.Strings.String
         Coq.Arith.Lt
         Coq.Arith.Compare_dec
         Coq.Lists.List

diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v b/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v
@@ -1,4 +1,4 @@
-Require Export Coq.Program.Program.
+Require Export Stdlib.Program.Program.
 Require Export CertifiedExtraction.Extraction.QueryStructures.Basics.
 Require Export CertifiedExtraction.Extraction.QueryStructures.TupleToListW.
 Require Export CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW.

diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v b/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v
@@ -176,7 +176,7 @@ Hint Rewrite
      @EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv_Characterisation
   : EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv.
 
-Require Import Coq.Strings.String.
+From Stdlib Require Import String.
 
 Lemma EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv:
   forall (n : nat) (lst : list (FiatWTuple n)) (ens : FiatWBag n),

diff --git a/src/CertifiedExtraction/FMapUtils.v b/src/CertifiedExtraction/FMapUtils.v
@@ -1,4 +1,4 @@
-Require Import Coq.FSets.FMaps.
+Require Import Stdlib.FSets.FMaps.
 Require Import CertifiedExtraction.PureUtils.
 
 Module WMoreFacts_fun (E:DecidableType) (Import M:WSfun E).

diff --git a/src/CertifiedExtraction/FacadeLemmas.v b/src/CertifiedExtraction/FacadeLemmas.v
@@ -3,7 +3,7 @@ Require Import
         CertifiedExtraction.PureUtils
         CertifiedExtraction.StringMapUtils
         CertifiedExtraction.FacadeUtils.
-Require Import Coq.Setoids.Setoid.
+From Stdlib Require Import Setoid.
 
 Lemma NotIn_not_mapsto_adt :
   forall {av} var (state: StringMap.t (Value av)),

diff --git a/src/CertifiedExtraction/FacadeNotations.v b/src/CertifiedExtraction/FacadeNotations.v
@@ -4,7 +4,7 @@ Require Import
         Bedrock.Platform.Cito.StringMap
         Bedrock.Platform.Cito.SyntaxExpr
         Bedrock.Memory.
-Require Import Coq.Strings.String.
+From Stdlib Require Import String.
 
 Notation "A ; B" := (Seq A B) (at level 201,
                                B at level 201,

diff --git a/src/CertifiedExtraction/FacadeUtils.v b/src/CertifiedExtraction/FacadeUtils.v
@@ -12,7 +12,7 @@ Require Import
         CertifiedExtraction.StringMapUtils
         CertifiedExtraction.PureFacadeLemmas.
 Require Import
-        Coq.Strings.String.
+        Stdlib.Strings.String.
 
 Require Export CertifiedExtraction.FacadeWrappers.
 

diff --git a/src/CertifiedExtraction/PropertiesOfTelescopes.v b/src/CertifiedExtraction/PropertiesOfTelescopes.v
@@ -18,7 +18,7 @@ Ltac TelEq_rel_t :=
          | _ => solve [intuition]
          end.
 
-Require Import Coq.Setoids.Setoid.
+From Stdlib Require Import Setoid.
 
 Lemma TelEq_refl {A ext}:
   Reflexive (@TelEq A ext).

diff --git a/src/CertifiedExtraction/PureFacadeLemmas.v b/src/CertifiedExtraction/PureFacadeLemmas.v
@@ -1,7 +1,7 @@
 Require Export Bedrock.Platform.Cito.StringMap Bedrock.Platform.Cito.StringMapFacts.
 Require Export Bedrock.Platform.Cito.SyntaxExpr Bedrock.Platform.Facade.DFacade.
 Require Import Bedrock.Platform.Facade.DFacadeFacts2.
-Require Import Coq.Setoids.Setoid.
+From Stdlib Require Import Setoid.
 
 Add Parametric Morphism {av} : (@eval av)
     with signature (StringMap.Equal ==> eq ==> eq)

diff --git a/src/CertifiedExtraction/RemoveSkips.v b/src/CertifiedExtraction/RemoveSkips.v
@@ -5,7 +5,7 @@ Require Import
         Fiat.CertifiedExtraction.FacadeUtils
         Fiat.CertifiedExtraction.FacadeNotations.
 
-Require Import Coq.Program.Program.
+From Stdlib Require Import Program.
 
 Definition Is_Skip : forall p, { p = Skip } + { p <> Skip }.
   destruct p;