Merge pull request #1093 from proux01/coq_19310

Adapt to coq/coq#19310

DOC.md

@@ -46,7 +46,7 @@ MetaCoq uses three types convertible to `string` which have a different intended
   E.g. `Datatypes.nat`
 
 - `kername` is a structured type of fully qualified names.
-  E.g. `Coq.Init.Datatypes.nat`
+  E.g. `Stdlib.Init.Datatypes.nat`
 
 Quoting always produce fully qualified names. On the converse, unquoting allow to
 have only partially qualified names and rely on Coq to resolve them. The commands

common/theories/config.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require CRelationClasses.
-From Coq Require Import Bool RelationClasses Btauto.
-From Coq.ssr Require Import ssreflect ssrbool.
+From Stdlib Require CRelationClasses.
+From Stdlib Require Import Bool RelationClasses Btauto.
+From Stdlib.ssr Require Import ssreflect ssrbool.
 
 Class checker_flags := {
   (* check_guard : bool ; *)

erasure-plugin/theories/Extraction.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import Ascii FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
+From Stdlib Require Import Ascii FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
 From MetaCoq.Utils Require Import utils.
 
 (** * Extraction setup for the erasure phase of template-coq.
@@ -41,5 +41,5 @@ Set Extraction Output Directory "src".
 
 Separate Extraction ErasureFunction.erase Erasure
          (* The following directives ensure separate extraction does not produce name clashes *)
-         Coq.Strings.String utils Template.UnivSubst ELiftSubst EGlobalEnv.
+         Stdlib.Strings.String utils Template.UnivSubst ELiftSubst EGlobalEnv.
 

examples/demo.v

@@ -19,7 +19,7 @@ MetaCoq Test Quote (let x := 2 in
               | S n => n
             end).
 
-MetaCoq Test Unquote (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 0 []).
+MetaCoq Test Unquote (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
 
 (** Build a definition **)
 Definition d : Ast.term.
@@ -71,7 +71,7 @@ MetaCoq Quote Definition eo_syntax := Eval compute in even.
 MetaCoq Quote Definition add'_syntax := Eval compute in add'.
 
 (** Reflecting definitions **)
-MetaCoq Unquote Definition zero_from_syntax := (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 0 []).
+MetaCoq Unquote Definition zero_from_syntax := (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
 Set Printing All.
 (* the function unquote_kn in reify.ml4 is not yet implemented *)
 
@@ -84,7 +84,7 @@ MetaCoq Unquote Definition add_from_syntax := add_syntax.
 MetaCoq Unquote Definition eo_from_syntax := eo_syntax.
 Print eo_from_syntax.
 
-Local Notation Nat_module := (MPfile ["Datatypes"; "Init"; "Coq"], "nat").
+Local Notation Nat_module := (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat").
 
 MetaCoq Unquote Definition two_from_syntax := (Ast.tApp (Ast.tConstruct (Kernames.mkInd Nat_module 0) 1 nil)
    (Ast.tApp (Ast.tConstruct (Kernames.mkInd Nat_module 0) 1 nil)
@@ -221,7 +221,7 @@ Definition printInductive (q : qualid): TemplateMonad unit :=
   | _ => tmFail ("[" ^ q ^ "] is not an inductive")
   end.
 
-MetaCoq Run (printInductive "Coq.Init.Datatypes.nat").
+MetaCoq Run (printInductive "Stdlib.Init.Datatypes.nat").
 MetaCoq Run (printInductive "nat").
 
 CoInductive cnat : Set :=  O :cnat | S : cnat -> cnat.
@@ -299,8 +299,8 @@ Definition printConstant' (name  : qualid): TemplateMonad unit :=
   | _ => tmFail ("[" ^ name ^ "] is not a constant")
   end.
 
-Fail MetaCoq Run (printInductive "Coq.Arith.PeanoNat.Nat.add").
-MetaCoq Run (printConstant' "Coq.Arith.PeanoNat.Nat.add").
+Fail MetaCoq Run (printInductive "Stdlib.Arith.PeanoNat.Nat.add").
+MetaCoq Run (printConstant' "Stdlib.Arith.PeanoNat.Nat.add").
 
 
 Fail MetaCoq Run (tmUnquoteTyped (nat -> nat) add_syntax >>= tmPrint).
@@ -409,6 +409,6 @@ Definition kername_of_qualid (q : qualid) : TemplateMonad kername :=
 
 MetaCoq Run (kername_of_qualid "add" >>= tmPrint).
 MetaCoq Run (kername_of_qualid "BinNat.N.add" >>= tmPrint).
-MetaCoq Run (kername_of_qualid "Coq.NArith.BinNatDef.N.add" >>= tmPrint).
+MetaCoq Run (kername_of_qualid "Stdlib.NArith.BinNatDef.N.add" >>= tmPrint).
 MetaCoq Run (kername_of_qualid "N.add" >>= tmPrint).
 Fail MetaCoq Run (kername_of_qualid "qlskf" >>= tmPrint).

examples/metacoq_tour.v

@@ -28,7 +28,7 @@ Definition foo := (fun x : nat => fun x : nat => x).
 MetaCoq Quote Definition reifx' := Eval compute in (fun x : nat => let y := x in fun x : nat => y).
 Print reifx'.
 MetaCoq Unquote Definition x :=
-  (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 0 []).
+  (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []).
 
 MetaCoq Run (tmBind (tmQuote (3 + 3)) tmPrint).
 

quotation/_CoqProject.in

@@ -11,15 +11,15 @@ theories/ToPCUIC/Common/Reflect.v
 theories/ToPCUIC/Common/Transform.v
 theories/ToPCUIC/Common/Universes.v
 theories/ToPCUIC/Common/config.v
-theories/ToPCUIC/Coq/Bool.v
-theories/ToPCUIC/Coq/FSets.v
-theories/ToPCUIC/Coq/Floats.v
-theories/ToPCUIC/Coq/Init.v
-theories/ToPCUIC/Coq/Lists.v
-theories/ToPCUIC/Coq/MSets.v
-theories/ToPCUIC/Coq/Numbers.v
-theories/ToPCUIC/Coq/Strings.v
-theories/ToPCUIC/Coq/ssr.v
+theories/ToPCUIC/Stdlib/Bool.v
+theories/ToPCUIC/Stdlib/FSets.v
+theories/ToPCUIC/Stdlib/Floats.v
+theories/ToPCUIC/Stdlib/Init.v
+theories/ToPCUIC/Stdlib/Lists.v
+theories/ToPCUIC/Stdlib/MSets.v
+theories/ToPCUIC/Stdlib/Numbers.v
+theories/ToPCUIC/Stdlib/Strings.v
+theories/ToPCUIC/Stdlib/ssr.v
 theories/ToPCUIC/Equations.v
 theories/ToPCUIC/Equations/Type.v
 theories/ToPCUIC/Init.v
@@ -59,21 +59,21 @@ theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.v
 theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.v
 theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v
 theories/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v
-theories/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.v
-theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapList/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetList/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/Structures/Equalities/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/Structures/Orders/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v
+theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v
 theories/ToPCUIC/QuotationOf/PCUIC/PCUICAst/Instances.v
 theories/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICConversion/Instances.v
 theories/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvTyping/Instances.v
@@ -127,15 +127,15 @@ theories/ToTemplate/Common/Reflect.v
 theories/ToTemplate/Common/Transform.v
 theories/ToTemplate/Common/Universes.v
 theories/ToTemplate/Common/config.v
-theories/ToTemplate/Coq/Bool.v
-theories/ToTemplate/Coq/FSets.v
-theories/ToTemplate/Coq/Floats.v
-theories/ToTemplate/Coq/Init.v
-theories/ToTemplate/Coq/Lists.v
-theories/ToTemplate/Coq/MSets.v
-theories/ToTemplate/Coq/Numbers.v
-theories/ToTemplate/Coq/Strings.v
-theories/ToTemplate/Coq/ssr.v
+theories/ToTemplate/Stdlib/Bool.v
+theories/ToTemplate/Stdlib/FSets.v
+theories/ToTemplate/Stdlib/Floats.v
+theories/ToTemplate/Stdlib/Init.v
+theories/ToTemplate/Stdlib/Lists.v
+theories/ToTemplate/Stdlib/MSets.v
+theories/ToTemplate/Stdlib/Numbers.v
+theories/ToTemplate/Stdlib/Strings.v
+theories/ToTemplate/Stdlib/ssr.v
 theories/ToTemplate/Equations.v
 theories/ToTemplate/Equations/Type.v
 theories/ToTemplate/Init.v
@@ -166,21 +166,21 @@ theories/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.v
 theories/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.v
 theories/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v
 theories/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v
-theories/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v
-theories/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.v
-theories/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.v
-theories/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v
-theories/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.v
-theories/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.v
-theories/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.v
-theories/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.v
-theories/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.v
-theories/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapList/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetList/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/Structures/Equalities/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/Structures/Orders/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v
+theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v
 theories/ToTemplate/QuotationOf/Template/Ast/Env/Instances.v
 theories/ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.v
 theories/ToTemplate/QuotationOf/Template/Ast/Instances.v

quotation/theories/README.md

@@ -68,7 +68,7 @@ Some design principles:
 
 - In most cases, inductive types are given explicit `ground_quotable` instances, while most defined constants are just made transparent to typeclass inference.  Defined constants containing `match`es or other constructions that make quoting non-trivial are the exception, and are given `ground_quotable` instances as well.  In general, either a constant is made transparent and added to the `quotation` unfolding hint database, *or* it is given a `ground_quotable` instance, (almost) never both.
 
-- Directory and file structure is mirrored between the `Quotation` development and the underlying Coq development for which quotation theory is being developed.  Sometimes directories are compressed into single files (e.g., [`ToTemplate/Coq/Init.v`](./ToTemplate/Coq/Init.v) contains quotation theory for everything in the `Coq.Init.*` namespace), and other times single files are expanded into a directory (e.g., [`ToTemplate/QuotationOf/Template/Ast/`](./ToTemplate/QuotationOf/Template/Ast/) contains `Foo/Instances.v` for every module `Foo` defined in `MetaCoq.Template.Ast` ([`template-coq/theories/Ast.v`](https://github.com/MetaCoq/metacoq/tree/coq-8.16/template-coq/theories/Ast.v))).  Directories are compressed into single files when the quotation theory is quick to typecheck and relatively short; files are expanded into directories when components of the quotation theory take a long time to typecheck, so that file-level parallelism can be better leveraged.
+- Directory and file structure is mirrored between the `Quotation` development and the underlying Coq development for which quotation theory is being developed.  Sometimes directories are compressed into single files (e.g., [`ToTemplate/Stdlib/Init.v`](./ToTemplate/Stdlib/Init.v) contains quotation theory for everything in the `Stdlib.Init.*` namespace), and other times single files are expanded into a directory (e.g., [`ToTemplate/QuotationOf/Template/Ast/`](./ToTemplate/QuotationOf/Template/Ast/) contains `Foo/Instances.v` for every module `Foo` defined in `MetaCoq.Template.Ast` ([`template-coq/theories/Ast.v`](https://github.com/MetaCoq/metacoq/tree/coq-8.16/template-coq/theories/Ast.v))).  Directories are compressed into single files when the quotation theory is quick to typecheck and relatively short; files are expanded into directories when components of the quotation theory take a long time to typecheck, so that file-level parallelism can be better leveraged.
 
 - When possible, we try to minimize the content in `ground_quotable` proofs (in particular, using named induction principles rather than bare fixpoints and avoiding excess conversion, when easy), so that proving that these constructions are well-typed is easier.  (This is still very much a work in progress, and principles making the proving of well-typedness easy are still in the works.)
 
@@ -102,7 +102,7 @@ Almost all other strucucture is mirrored between the `ToTemplate/` and `ToPCUIC/
 
 - [`ToTemplate/QuotationOf/`](./ToTemplate/QuotationOf/), [`ToPCUIC/QuotationOf/`](./ToPCUIC/QuotationOf/) - These directories develop `quotation_of` instances for various `Module Type`s and functors.  The various `Sig.v` files contain `Module Type`s declaring the instances, while the various `Instances.v` files contain the definitions of `Module`s having these `Module Type`s defining the `quotation_of` instances.  The `Module`s in `Instances.v` files *do not* export `Instance`s, while the `Module Type`s in `Sig.v` files *do*; if the concrete constant needs to be quoted, it can be quoted with `<% ... %>` directly and does not need an instance; when functors take in a `Module Type` argument, by contrast, they do need access to the instances declared.  When `Module`s are nested inside `Module Type`s, the top-level `Module Type` exports all declared instances in the submodules.  Nearly all declarations and definitions in files under `QuotationOf` are fully automated; when well-typedness is eventually proven, that should be fully automated as well for these directories, likely by invoking the Safe Checker.
 
-- Under `ToTemplate/` / `ToPCUIC/`, folders `Coq/`, `Equations/`, `Utils/`, `Common/`, and `Template/` or `PCUIC/` develop the `ground_quotable` instances for `Coq.*`, `Equations.*`, `MetaCoq.Utils.*`, `MetaCoq.Common.*`, and `MetaCoq.Template.*` or `MetaCoq.PCUIC.*`, respectively.  In `Coq/` and `Equations/`, generally one file is given to each folder of the underlying development; in `Utils/`, `Common/`, `Template/`, and `PCUIC/`, files generally correspond one-to-one with the underlying development.
+- Under `ToTemplate/` / `ToPCUIC/`, folders `Stdlib/`, `Equations/`, `Utils/`, `Common/`, and `Template/` or `PCUIC/` develop the `ground_quotable` instances for `Stdlib.*`, `Equations.*`, `MetaCoq.Utils.*`, `MetaCoq.Common.*`, and `MetaCoq.Template.*` or `MetaCoq.PCUIC.*`, respectively.  In `Stdlib/` and `Equations/`, generally one file is given to each folder of the underlying development; in `Utils/`, `Common/`, `Template/`, and `PCUIC/`, files generally correspond one-to-one with the underlying development.
 
 ## Debugging Suggestions
 

quotation/theories/ToPCUIC/Common/BasicAst.v

@@ -1,5 +1,5 @@
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Floats Coq.Numbers.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Floats Stdlib.Numbers.
 From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) utils.
 From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Kernames.
 From MetaCoq.Common Require Import BasicAst.

quotation/theories/ToPCUIC/Common/Environment.v

@@ -2,7 +2,7 @@ From Coq Require Import Structures.Equalities Lists.List Lists.ListDec.
 From MetaCoq.Utils Require Import MCProd All_Forall ReflectEq MCRelations MCReflect.
 From MetaCoq.Common Require Import Environment Universes.
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.ssr utils BasicAst Primitive Universes Kernames.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.ssr utils BasicAst Primitive Universes Kernames.
 From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) MCOption MCProd All_Forall.
 From MetaCoq.Quotation.ToPCUIC.QuotationOf.Common Require Import Environment.Sig.
 

quotation/theories/ToPCUIC/Common/EnvironmentTyping.v

@@ -1,6 +1,6 @@
 From MetaCoq.Common Require Import BasicAst Environment EnvironmentTyping Universes.
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists Coq.ssr.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.ssr.
 From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall MCOption.
 From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) config BasicAst Kernames Universes Environment.
 From MetaCoq.Quotation.ToPCUIC.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig.

quotation/theories/ToPCUIC/Common/Kernames.v

@@ -1,6 +1,6 @@
 From MetaCoq.Common Require Import Kernames.
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.MSets Coq.FSets bytestring.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.MSets Stdlib.FSets bytestring.
 From MetaCoq.Quotation.ToPCUIC.QuotationOf.Common Require Import Kernames.Instances.
 
 #[local] Hint Unfold ident qualid dirpath kername : quotation.

quotation/theories/ToPCUIC/Common/Primitive.v

@@ -1,4 +1,4 @@
-From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init.
+From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init.
 From MetaCoq.Common Require Import Primitive.
 
 #[export] Instance quote_prim_tag : ground_quotable prim_tag := ltac:(destruct 1; exact _).

quotation/theories/ToPCUIC/Common/Universes.v

@@ -1,5 +1,5 @@
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC.Coq Require Import (hints) Init MSets Numbers.
+From MetaCoq.Quotation.ToPCUIC.Stdlib Require Import (hints) Init MSets Numbers.
 From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) MCOption bytestring.
 From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) BasicAst config.
 From MetaCoq.Quotation.ToPCUIC.QuotationOf.Common Require Import Universes.Instances.

quotation/theories/ToPCUIC/Common/config.v

@@ -1,4 +1,4 @@
-From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init.
+From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init.
 From MetaCoq.Common Require Import config.
 
 #[export] Instance quote_checker_flags : ground_quotable checker_flags := ltac:(destruct 1; exact _).

quotation/theories/ToPCUIC/Equations.v

@@ -1,5 +1,5 @@
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init.
 From Equations Require Import Init.
 
 Local Set Universe Polymorphism.

quotation/theories/ToPCUIC/Equations/Type.v

@@ -1,5 +1,5 @@
 From MetaCoq.Quotation.ToPCUIC Require Import Init.
-From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Equations.
+From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Equations.
 From Equations.Type Require Import -(notations) Logic Relation.
 
 Local Set Universe Polymorphism.