From ddcd8846715802c257f737e5d56ce8db31bb8d02 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 12 Jul 2024 17:33:25 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19310 --- DOC.md | 2 +- common/theories/config.v | 6 +- erasure-plugin/theories/Extraction.v | 4 +- examples/demo.v | 14 +-- examples/metacoq_tour.v | 2 +- quotation/_CoqProject.in | 96 +++++++++---------- quotation/theories/README.md | 4 +- quotation/theories/ToPCUIC/Common/BasicAst.v | 2 +- .../theories/ToPCUIC/Common/Environment.v | 2 +- .../ToPCUIC/Common/EnvironmentTyping.v | 2 +- quotation/theories/ToPCUIC/Common/Kernames.v | 2 +- quotation/theories/ToPCUIC/Common/Primitive.v | 2 +- quotation/theories/ToPCUIC/Common/Universes.v | 2 +- quotation/theories/ToPCUIC/Common/config.v | 2 +- quotation/theories/ToPCUIC/Equations.v | 2 +- quotation/theories/ToPCUIC/Equations/Type.v | 2 +- quotation/theories/ToPCUIC/Init.v | 4 +- quotation/theories/ToPCUIC/PCUIC/PCUICAst.v | 2 +- .../ToPCUIC/PCUIC/PCUICCumulativitySpec.v | 2 +- .../theories/ToPCUIC/PCUIC/PCUICEquality.v | 4 +- .../theories/ToPCUIC/PCUIC/PCUICReduction.v | 2 +- .../theories/ToPCUIC/PCUIC/PCUICTyping.v | 2 +- .../ToPCUIC/PCUIC/Syntax/PCUICCases.v | 2 +- .../ToPCUIC/PCUIC/utils/PCUICAstUtils.v | 2 +- .../ToPCUIC/PCUIC/utils/PCUICPrimitive.v | 2 +- .../Common/Kernames/Kername/Instances.v | 2 +- .../Common/Kernames/KernameMap/Instances.v | 4 +- .../Kernames/KernameMapFact/Instances.v | 2 +- .../Common/Kernames/KernameSet/Instances.v | 2 +- .../Kernames/KernameSetOrdProp/Instances.v | 4 +- .../Universes/ConstraintSet/Instances.v | 2 +- .../ConstraintSetOrdProp/Instances.v | 4 +- .../Common/Universes/Level/Instances.v | 2 +- .../Common/Universes/LevelExpr/Instances.v | 2 +- .../Common/Universes/LevelExprSet/Instances.v | 2 +- .../Universes/LevelExprSetOrdProp/Instances.v | 4 +- .../Common/Universes/LevelSet/Instances.v | 2 +- .../Universes/LevelSetOrdProp/Instances.v | 4 +- .../Universes/UnivConstraint/Instances.v | 2 +- .../{Coq => Stdlib}/FSets/FMapAVL/Sig.v | 4 +- .../{Coq => Stdlib}/FSets/FMapFacts/Sig.v | 0 .../{Coq => Stdlib}/FSets/FMapInterface/Sig.v | 0 .../{Coq => Stdlib}/FSets/FMapList/Sig.v | 2 +- .../{Coq => Stdlib}/MSets/MSetAVL/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetDecide/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetFacts/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetInterface/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetList/Sig.v | 2 +- .../Stdlib}/MSets/MSetProperties/Sig.v | 6 +- .../Structures/Equalities/Sig.v | 0 .../{Coq => Stdlib}/Structures/Orders/Sig.v | 2 +- .../Structures/OrdersAlt/Sig.v | 2 +- .../Structures/OrdersFacts/Sig.v | 2 +- .../Structures/OrdersTac/Sig.v | 2 +- .../theories/ToPCUIC/{Coq => Stdlib}/Bool.v | 2 +- .../theories/ToPCUIC/{Coq => Stdlib}/FSets.v | 6 +- .../theories/ToPCUIC/{Coq => Stdlib}/Floats.v | 2 +- .../theories/ToPCUIC/{Coq => Stdlib}/Init.v | 0 .../theories/ToPCUIC/{Coq => Stdlib}/Lists.v | 2 +- .../theories/ToPCUIC/{Coq => Stdlib}/MSets.v | 6 +- .../ToPCUIC/{Coq => Stdlib}/Numbers.v | 2 +- .../ToPCUIC/{Coq => Stdlib}/Strings.v | 2 +- .../theories/ToPCUIC/{Coq => Stdlib}/ssr.v | 2 +- quotation/theories/ToPCUIC/Utils/All_Forall.v | 2 +- quotation/theories/ToPCUIC/Utils/MCArith.v | 2 +- quotation/theories/ToPCUIC/Utils/MCList.v | 2 +- quotation/theories/ToPCUIC/Utils/MCOption.v | 2 +- quotation/theories/ToPCUIC/Utils/MCProd.v | 2 +- quotation/theories/ToPCUIC/Utils/MCReflect.v | 2 +- quotation/theories/ToPCUIC/Utils/ReflectEq.v | 2 +- quotation/theories/ToPCUIC/Utils/bytestring.v | 2 +- quotation/theories/ToPCUIC/Utils/utils.v | 2 +- .../theories/ToTemplate/Common/BasicAst.v | 2 +- .../theories/ToTemplate/Common/Environment.v | 2 +- .../ToTemplate/Common/EnvironmentTyping.v | 2 +- .../theories/ToTemplate/Common/Kernames.v | 2 +- .../theories/ToTemplate/Common/Primitive.v | 2 +- .../theories/ToTemplate/Common/Universes.v | 2 +- quotation/theories/ToTemplate/Common/config.v | 2 +- quotation/theories/ToTemplate/Equations.v | 2 +- .../theories/ToTemplate/Equations/Type.v | 2 +- quotation/theories/ToTemplate/Init.v | 4 +- .../Common/Kernames/Kername/Instances.v | 2 +- .../Common/Kernames/KernameMap/Instances.v | 4 +- .../Kernames/KernameMapFact/Instances.v | 2 +- .../Common/Kernames/KernameSet/Instances.v | 2 +- .../Kernames/KernameSetOrdProp/Instances.v | 4 +- .../Universes/ConstraintSet/Instances.v | 2 +- .../ConstraintSetOrdProp/Instances.v | 4 +- .../Common/Universes/Level/Instances.v | 2 +- .../Common/Universes/LevelExpr/Instances.v | 2 +- .../Common/Universes/LevelExprSet/Instances.v | 2 +- .../Universes/LevelExprSetOrdProp/Instances.v | 4 +- .../Common/Universes/LevelSet/Instances.v | 2 +- .../Universes/LevelSetOrdProp/Instances.v | 4 +- .../Universes/UnivConstraint/Instances.v | 2 +- .../{Coq => Stdlib}/FSets/FMapAVL/Sig.v | 4 +- .../{Coq => Stdlib}/FSets/FMapFacts/Sig.v | 0 .../{Coq => Stdlib}/FSets/FMapInterface/Sig.v | 0 .../{Coq => Stdlib}/FSets/FMapList/Sig.v | 2 +- .../{Coq => Stdlib}/MSets/MSetAVL/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetDecide/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetFacts/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetInterface/Sig.v | 0 .../{Coq => Stdlib}/MSets/MSetList/Sig.v | 2 +- .../Stdlib}/MSets/MSetProperties/Sig.v | 6 +- .../Structures/Equalities/Sig.v | 0 .../{Coq => Stdlib}/Structures/Orders/Sig.v | 2 +- .../Structures/OrdersAlt/Sig.v | 2 +- .../Structures/OrdersFacts/Sig.v | 2 +- .../Structures/OrdersTac/Sig.v | 2 +- .../ToTemplate/{Coq => Stdlib}/Bool.v | 2 +- .../ToTemplate/{Coq => Stdlib}/FSets.v | 6 +- .../ToTemplate/{Coq => Stdlib}/Floats.v | 2 +- .../ToTemplate/{Coq => Stdlib}/Init.v | 0 .../ToTemplate/{Coq => Stdlib}/Lists.v | 2 +- .../ToTemplate/{Coq => Stdlib}/MSets.v | 6 +- .../ToTemplate/{Coq => Stdlib}/Numbers.v | 2 +- .../ToTemplate/{Coq => Stdlib}/Strings.v | 2 +- .../theories/ToTemplate/{Coq => Stdlib}/ssr.v | 2 +- quotation/theories/ToTemplate/Template/Ast.v | 2 +- .../theories/ToTemplate/Template/AstUtils.v | 2 +- .../ToTemplate/Template/TermEquality.v | 4 +- .../theories/ToTemplate/Template/Typing.v | 2 +- .../theories/ToTemplate/Template/TypingWf.v | 2 +- .../theories/ToTemplate/Template/WfAst.v | 2 +- .../theories/ToTemplate/Utils/All_Forall.v | 2 +- quotation/theories/ToTemplate/Utils/MCArith.v | 2 +- quotation/theories/ToTemplate/Utils/MCList.v | 2 +- .../theories/ToTemplate/Utils/MCOption.v | 2 +- quotation/theories/ToTemplate/Utils/MCProd.v | 2 +- .../theories/ToTemplate/Utils/MCReflect.v | 2 +- .../theories/ToTemplate/Utils/ReflectEq.v | 2 +- .../theories/ToTemplate/Utils/bytestring.v | 2 +- quotation/theories/ToTemplate/Utils/utils.v | 2 +- safechecker-plugin/theories/Extraction.v | 4 +- safechecker/theories/PCUICSafeChecker.v | 2 +- safechecker/theories/PCUICTypeChecker.v | 4 +- template-coq/theories/Constants.v | 60 ++++++------ test-suite/erasure_test.v | 10 +- test-suite/extractable.v | 6 +- test-suite/modules_sections.v | 6 +- test-suite/proj.v | 4 +- test-suite/safechecker_test.v | 8 +- test-suite/unfold.v | 2 +- test-suite/univ.v | 12 +-- test-suite/vs.v | 12 +-- translations/MiniHoTT.v | 2 +- translations/MiniHoTT_paths.v | 2 +- translations/param_cheap_packed.v | 18 ++-- utils/theories/MCList.v | 6 +- 151 files changed, 283 insertions(+), 283 deletions(-) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/FSets/FMapAVL/Sig.v (86%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/FSets/FMapFacts/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/FSets/FMapInterface/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/FSets/FMapList/Sig.v (87%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/MSets/MSetAVL/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/MSets/MSetDecide/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/MSets/MSetFacts/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/MSets/MSetInterface/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/MSets/MSetList/Sig.v (92%) rename quotation/theories/{ToTemplate/QuotationOf/Coq => ToPCUIC/QuotationOf/Stdlib}/MSets/MSetProperties/Sig.v (87%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/Structures/Equalities/Sig.v (100%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/Structures/Orders/Sig.v (99%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/Structures/OrdersAlt/Sig.v (98%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/Structures/OrdersFacts/Sig.v (97%) rename quotation/theories/ToPCUIC/QuotationOf/{Coq => Stdlib}/Structures/OrdersTac/Sig.v (95%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Bool.v (89%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/FSets.v (93%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Floats.v (90%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Init.v (100%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Lists.v (98%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/MSets.v (97%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Numbers.v (96%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/Strings.v (80%) rename quotation/theories/ToPCUIC/{Coq => Stdlib}/ssr.v (96%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/FSets/FMapAVL/Sig.v (85%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/FSets/FMapFacts/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/FSets/FMapInterface/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/FSets/FMapList/Sig.v (87%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/MSets/MSetAVL/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/MSets/MSetDecide/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/MSets/MSetFacts/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/MSets/MSetInterface/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/MSets/MSetList/Sig.v (92%) rename quotation/theories/{ToPCUIC/QuotationOf/Coq => ToTemplate/QuotationOf/Stdlib}/MSets/MSetProperties/Sig.v (82%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/Structures/Equalities/Sig.v (100%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/Structures/Orders/Sig.v (99%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/Structures/OrdersAlt/Sig.v (98%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/Structures/OrdersFacts/Sig.v (97%) rename quotation/theories/ToTemplate/QuotationOf/{Coq => Stdlib}/Structures/OrdersTac/Sig.v (94%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Bool.v (88%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/FSets.v (93%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Floats.v (90%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Init.v (100%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Lists.v (98%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/MSets.v (97%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Numbers.v (96%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/Strings.v (79%) rename quotation/theories/ToTemplate/{Coq => Stdlib}/ssr.v (96%) diff --git a/DOC.md b/DOC.md index bb585b42b..399bf42a6 100644 --- a/DOC.md +++ b/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 diff --git a/common/theories/config.v b/common/theories/config.v index eb89636e3..f3285f057 100644 --- a/common/theories/config.v +++ b/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 ; *) diff --git a/erasure-plugin/theories/Extraction.v b/erasure-plugin/theories/Extraction.v index 99ccf0bc7..e36377c29 100644 --- a/erasure-plugin/theories/Extraction.v +++ b/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. diff --git a/examples/demo.v b/examples/demo.v index 0b6e0ddf1..12fd705f6 100644 --- a/examples/demo.v +++ b/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). diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v index 3830aa3de..289d2edb3 100644 --- a/examples/metacoq_tour.v +++ b/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). diff --git a/quotation/_CoqProject.in b/quotation/_CoqProject.in index 612b4dc03..692472415 100644 --- a/quotation/_CoqProject.in +++ b/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 diff --git a/quotation/theories/README.md b/quotation/theories/README.md index 5cf620713..162eec4fc 100644 --- a/quotation/theories/README.md +++ b/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 diff --git a/quotation/theories/ToPCUIC/Common/BasicAst.v b/quotation/theories/ToPCUIC/Common/BasicAst.v index f0bc398f9..934bc2507 100644 --- a/quotation/theories/ToPCUIC/Common/BasicAst.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Common/Environment.v b/quotation/theories/ToPCUIC/Common/Environment.v index ebcf16db8..713bbb07e 100644 --- a/quotation/theories/ToPCUIC/Common/Environment.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Common/EnvironmentTyping.v b/quotation/theories/ToPCUIC/Common/EnvironmentTyping.v index e138b1418..6abb61372 100644 --- a/quotation/theories/ToPCUIC/Common/EnvironmentTyping.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Common/Kernames.v b/quotation/theories/ToPCUIC/Common/Kernames.v index b59d900d1..b7318f9e0 100644 --- a/quotation/theories/ToPCUIC/Common/Kernames.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Common/Primitive.v b/quotation/theories/ToPCUIC/Common/Primitive.v index 2b2bdfdc3..a4d8846c4 100644 --- a/quotation/theories/ToPCUIC/Common/Primitive.v +++ b/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 _). diff --git a/quotation/theories/ToPCUIC/Common/Universes.v b/quotation/theories/ToPCUIC/Common/Universes.v index 3077ec65a..a9531335c 100644 --- a/quotation/theories/ToPCUIC/Common/Universes.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Common/config.v b/quotation/theories/ToPCUIC/Common/config.v index e1fdebeae..e9a57a051 100644 --- a/quotation/theories/ToPCUIC/Common/config.v +++ b/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 _). diff --git a/quotation/theories/ToPCUIC/Equations.v b/quotation/theories/ToPCUIC/Equations.v index aa0351579..703eaaa04 100644 --- a/quotation/theories/ToPCUIC/Equations.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Equations/Type.v b/quotation/theories/ToPCUIC/Equations/Type.v index e47b310ae..81948f61a 100644 --- a/quotation/theories/ToPCUIC/Equations/Type.v +++ b/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. diff --git a/quotation/theories/ToPCUIC/Init.v b/quotation/theories/ToPCUIC/Init.v index 135434a7c..a4191a976 100644 --- a/quotation/theories/ToPCUIC/Init.v +++ b/quotation/theories/ToPCUIC/Init.v @@ -5,7 +5,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICMonadAst. From MetaCoq.TemplatePCUIC Require Import PCUICTemplateMonad Loader. From MetaCoq.Quotation Require Export CommonUtils. Require Import Equations.Prop.Classes. -Require Import Coq.Lists.List. +Require Import Stdlib.Lists.List. Export TemplateMonad.Common (export, local, global). Import ListNotations. @@ -596,5 +596,5 @@ Global Arguments tmDeclareQuotationOfModule {_%_bool} _ _ _%_bs. (* Require Import MSetPositive. Instance: debug_opt := true. -MetaCoq Run (tmMakeQuotationOfModule None "Coq.MSets.MSetPositive.PositiveSet"%bs). +MetaCoq Run (tmMakeQuotationOfModule None "Stdlib.MSets.MSetPositive.PositiveSet"%bs). *) diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v b/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v index cacfba567..3c08e43e1 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst Syntax.PCUICReflect Syntax.PCUICInduction. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Universes BasicAst Kernames. From MetaCoq.Quotation.ToPCUIC.Common Require Import Environment EnvironmentTyping. From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) utils.PCUICPrimitive. diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICCumulativitySpec.v b/quotation/theories/ToPCUIC/PCUIC/PCUICCumulativitySpec.v index 2522a9241..48e0fb9bd 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICCumulativitySpec.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICCumulativitySpec.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICCumulativitySpec. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists. From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) config BasicAst Universes Kernames. From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst PCUICEquality utils.PCUICPrimitive. diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v b/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v index ba56223fd..e22708e51 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICEquality.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICEquality. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) utils All_Forall. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) config Reflect Environment Universes BasicAst Kernames. From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst utils.PCUICPrimitive (*PCUICAstUtils*) (*Induction*). @@ -20,7 +20,7 @@ Section with_R. #[export] Instance quote_cmp_opt_variance {pb v u u'} (subr : RelationClasses.subrelation (cmp_universe Conv) (cmp_universe pb)) : ground_quotable (@cmp_opt_variance cmp_universe pb v u u'). Proof using cmp_universe qRe quoteRe. destruct v; cbv [cmp_opt_variance]; try exact _. - eapply Coq.Init.quote_or_dec; try exact _. + eapply Stdlib.Init.quote_or_dec; try exact _. now apply cmp_opt_variance_var_dec. Defined. diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v b/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v index 24a4ef0fe..0cf355414 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICReduction.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICReduction. 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 MetaCoq.Quotation.ToPCUIC Require Import (hints) Equations.Type. From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) BasicAst Universes Kernames. diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v index d03f775ca..d8343e844 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICTyping.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICTyping. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) utils All_Forall (* MCProd*). From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) config BasicAst Universes Kernames Environment EnvironmentTyping Primitive Reflect. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Environment EnvironmentTyping. diff --git a/quotation/theories/ToPCUIC/PCUIC/Syntax/PCUICCases.v b/quotation/theories/ToPCUIC/PCUIC/Syntax/PCUICCases.v index fd8478295..d40874283 100644 --- a/quotation/theories/ToPCUIC/PCUIC/Syntax/PCUICCases.v +++ b/quotation/theories/ToPCUIC/PCUIC/Syntax/PCUICCases.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAst Syntax.PCUICCases. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Lists(* Coq.Numbers Coq.Floats*). +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Lists(* Stdlib.Numbers Stdlib.Floats*). From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) (*utils*) All_Forall (* MCProd*). From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) (*config*) BasicAst Kernames (*Universes Environment EnvironmentTyping Primitive Reflect*). From MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst. diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICAstUtils.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICAstUtils.v index 17586cb4c..50d39ff92 100644 --- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICAstUtils.v +++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICAstUtils.v @@ -1,6 +1,6 @@ From MetaCoq.PCUIC Require Import PCUICAstUtils. 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 MetaCoq.Quotation.ToPCUIC.PCUIC Require Import (hints) PCUICAst. #[export] Instance quote_mkApps_spec {f args fargs1 args2 fargs} : ground_quotable (@mkApps_spec f args fargs1 args2 fargs) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v index 3ca579c47..892f59106 100644 --- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v +++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v @@ -1,7 +1,7 @@ From MetaCoq.Utils.MCTactics Require Import DestructHead UniquePose. From MetaCoq.PCUIC Require Import utils.PCUICPrimitive. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToPCUIC.Common Require Import (hints) Universes Primitive. From MetaCoq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.v index 1440c8178..538f38445 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.v index 8324882fc..9d11789b4 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.FSets Require Import FMapAVL.Sig FMapList.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.FSets Require Import FMapAVL.Sig FMapList.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.v index 1798874e2..ba97c5ddb 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.FSets Require Import FMapFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.FSets Require Import FMapFacts.Sig. Module qKernameMapFact. Module qF <: QuotationOfWFacts_fun Kername.OT KernameMap KernameMapFact.F. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.v index 7e1bf6604..ec8a24a3e 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qKernameSet <: MSetAVL.QuotationOfMake Kername KernameSet. MetaCoq Run (tmMakeQuotationOfModule everything None "KernameSet"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v index c0b7dd971..e69ef1779 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.v index 61214fae2..08f5eab9b 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qConstraintSet <: MSetAVL.QuotationOfMake UnivConstraint ConstraintSet. MetaCoq Run (tmMakeQuotationOfModule everything None "ConstraintSet"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v index 55ac3580e..a978ca384 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.v index 88fee5c91..7889cd7fc 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.v index 08cb57d57..1d2aecad6 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.v index 015f79789..30f47b955 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetList.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetList.Sig. Module qLevelExprSet <: MSetList.QuotationOfMakeWithLeibniz LevelExpr LevelExprSet. MetaCoq Run (tmMakeQuotationOfModule everything None "LevelExprSet"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v index 0a1a04c9c..66ba4e9cd 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.v index 32ca446ca..e6c688f69 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qLevelSet <: MSetAVL.QuotationOfMake Level LevelSet. MetaCoq Run (tmMakeQuotationOfModule everything None "LevelSet"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v index 3a14caed1..2c84c43e9 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v index 4f3952949..92cfaa5c0 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v similarity index 86% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v index 6dd53130b..eabe330f5 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v @@ -2,8 +2,8 @@ From Coq.FSets Require Import FMapAVL. From Coq.Structures Require Import Equalities OrdersAlt. From MetaCoq.Utils Require Import MCFSets. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.FSets Require Import FMapList.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.FSets Require Import FMapList.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapList/Sig.v similarity index 87% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapList/Sig.v index 0ab79f89b..32cdde1b7 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/FSets/FMapList/Sig.v @@ -2,7 +2,7 @@ From Coq.FSets Require Import FMapList. From Coq.Structures Require Import Equalities OrdersAlt. From MetaCoq.Utils Require Import MCFSets. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetList/Sig.v similarity index 92% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetList/Sig.v index fbc2d61ce..a6c66f2b8 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetList/Sig.v @@ -2,7 +2,7 @@ From Coq.Structures Require Import Equalities Orders. From Coq.MSets Require Import MSetList. From MetaCoq.Utils Require Import MCMSets. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetInterface.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetInterface.Sig. Module Type QuotationOfOrderedTypeWithLeibniz (O : OrderedTypeWithLeibniz). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "O"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v similarity index 87% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v index 9a9b4e890..ea47c93cb 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v @@ -1,8 +1,8 @@ From Coq.MSets Require Import MSetProperties. From MetaCoq.Utils Require Import MCMSets. -From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetFacts.Sig MSetDecide.Sig. +From MetaCoq.Quotation.ToPCUIC Require Import Init. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import OrdersFacts.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetFacts.Sig MSetDecide.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/Equalities/Sig.v similarity index 100% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/Equalities/Sig.v diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/Orders/Sig.v similarity index 99% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/Orders/Sig.v index 115242f56..4215548fa 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/Orders/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Orders. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq Require Export Structures.Equalities.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib Require Export Structures.Equalities.Sig. Module Type QuotationOfHasLt (Import T : Typ) (Import E : HasLt T). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "E"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v similarity index 98% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v index 77ba03bdf..8741e17eb 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v @@ -1,7 +1,7 @@ From Coq.Structures Require Import Equalities OrdersAlt. From Coq.Structures Require OrderedType. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v similarity index 97% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v index 37afe1a9b..c811c8f60 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Equalities Orders OrdersFacts. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Module Type QuotationOfCompareFacts (O : DecStrOrder) (F : CompareFacts O). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "F"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v similarity index 95% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.v rename to quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v index 75b3842a8..fad3e214b 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Equalities Orders OrdersTac. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Module Type QuotationOfIsTotalOrder (O : EqLtLe) (S : IsTotalOrder O) := QuotationOfIsEq O S <+ QuotationOfIsStrOrder O S <+ QuotationOfLeIsLtEq O S <+ QuotationOfLtIsTotal O S. diff --git a/quotation/theories/ToPCUIC/Coq/Bool.v b/quotation/theories/ToPCUIC/Stdlib/Bool.v similarity index 89% rename from quotation/theories/ToPCUIC/Coq/Bool.v rename to quotation/theories/ToPCUIC/Stdlib/Bool.v index 5c1b5bca5..f42ed3203 100644 --- a/quotation/theories/ToPCUIC/Coq/Bool.v +++ b/quotation/theories/ToPCUIC/Stdlib/Bool.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From Coq.Bool Require Import Bool IfProp. #[export] Instance quote_reflect {P : Prop} {qP : quotation_of P} {quoteP : ground_quotable P} {quote_negP : ground_quotable (~P)} {b} : ground_quotable (reflect P b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Coq/FSets.v b/quotation/theories/ToPCUIC/Stdlib/FSets.v similarity index 93% rename from quotation/theories/ToPCUIC/Coq/FSets.v rename to quotation/theories/ToPCUIC/Stdlib/FSets.v index f927cbc15..f3487d27a 100644 --- a/quotation/theories/ToPCUIC/Coq/FSets.v +++ b/quotation/theories/ToPCUIC/Stdlib/FSets.v @@ -1,9 +1,9 @@ From Coq Require Import Structures.Equalities Structures.OrdersAlt FMapInterface FMapList FMapAVL FMapFullAVL FMapFacts. From MetaCoq.Utils Require Import MCUtils MCFSets. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Numbers Coq.Init Coq.Lists. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.FSets Require Import FMapInterface.Sig FMapFacts.Sig FMapAVL.Sig FMapList.Sig. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Numbers Stdlib.Init Stdlib.Lists. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.FSets Require Import FMapInterface.Sig FMapFacts.Sig FMapAVL.Sig FMapList.Sig. From MetaCoq.Quotation.ToPCUIC.QuotationOf.Utils Require Import MCFSets.Sig. #[export] Hint Unfold Int.Z_as_Int.t : quotation. diff --git a/quotation/theories/ToPCUIC/Coq/Floats.v b/quotation/theories/ToPCUIC/Stdlib/Floats.v similarity index 90% rename from quotation/theories/ToPCUIC/Coq/Floats.v rename to quotation/theories/ToPCUIC/Stdlib/Floats.v index c76b711dc..e51d95808 100644 --- a/quotation/theories/ToPCUIC/Coq/Floats.v +++ b/quotation/theories/ToPCUIC/Stdlib/Floats.v @@ -1,6 +1,6 @@ From Coq.Floats Require Import FloatClass Floats PrimFloat SpecFloat. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Init Coq.Numbers. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Numbers. #[export] Instance quote_float : ground_quotable float := fun f => PCUICAst.tFloat f. #[export] Instance quote_float_class : ground_quotable float_class := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Coq/Init.v b/quotation/theories/ToPCUIC/Stdlib/Init.v similarity index 100% rename from quotation/theories/ToPCUIC/Coq/Init.v rename to quotation/theories/ToPCUIC/Stdlib/Init.v diff --git a/quotation/theories/ToPCUIC/Coq/Lists.v b/quotation/theories/ToPCUIC/Stdlib/Lists.v similarity index 98% rename from quotation/theories/ToPCUIC/Coq/Lists.v rename to quotation/theories/ToPCUIC/Stdlib/Lists.v index ad650801f..e2bab5dfc 100644 --- a/quotation/theories/ToPCUIC/Coq/Lists.v +++ b/quotation/theories/ToPCUIC/Stdlib/Lists.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List. Require Import Coq.Lists.ListDec. From MetaCoq.Utils Require Import ReflectEq. 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.Prop Require Import Classes. Import ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToPCUIC/Coq/MSets.v b/quotation/theories/ToPCUIC/Stdlib/MSets.v similarity index 97% rename from quotation/theories/ToPCUIC/Coq/MSets.v rename to quotation/theories/ToPCUIC/Stdlib/MSets.v index f3da246a8..48410fa03 100644 --- a/quotation/theories/ToPCUIC/Coq/MSets.v +++ b/quotation/theories/ToPCUIC/Stdlib/MSets.v @@ -1,9 +1,9 @@ From Coq Require Import MSetInterface MSetList MSetAVL MSetFacts MSetProperties MSetDecide. From MetaCoq.Utils Require Import MCMSets. From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC Require Import (hints) Coq.Numbers Coq.Init Coq.Lists. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import Orders.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetInterface.Sig MSetProperties.Sig MSetAVL.Sig MSetList.Sig. +From MetaCoq.Quotation.ToPCUIC Require Import (hints) Stdlib.Numbers Stdlib.Init Stdlib.Lists. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.Structures Require Import Orders.Sig. +From MetaCoq.Quotation.ToPCUIC.QuotationOf.Stdlib.MSets Require Import MSetInterface.Sig MSetProperties.Sig MSetAVL.Sig MSetList.Sig. From MetaCoq.Quotation.ToPCUIC.QuotationOf.Utils Require Import MCMSets.Sig. #[export] Hint Unfold Int.Z_as_Int.t : quotation. diff --git a/quotation/theories/ToPCUIC/Coq/Numbers.v b/quotation/theories/ToPCUIC/Stdlib/Numbers.v similarity index 96% rename from quotation/theories/ToPCUIC/Coq/Numbers.v rename to quotation/theories/ToPCUIC/Stdlib/Numbers.v index 69ef3b868..65c0e8ea4 100644 --- a/quotation/theories/ToPCUIC/Coq/Numbers.v +++ b/quotation/theories/ToPCUIC/Stdlib/Numbers.v @@ -6,7 +6,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts . From Coq Require Import ZArith. -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. #[export] Instance quote_positive : ground_quotable positive := ltac:(induction 1; exact _). #[export] Instance quote_N : ground_quotable N := ltac:(induction 1; exact _). diff --git a/quotation/theories/ToPCUIC/Coq/Strings.v b/quotation/theories/ToPCUIC/Stdlib/Strings.v similarity index 80% rename from quotation/theories/ToPCUIC/Coq/Strings.v rename to quotation/theories/ToPCUIC/Stdlib/Strings.v index cc36762bb..b73848459 100644 --- a/quotation/theories/ToPCUIC/Coq/Strings.v +++ b/quotation/theories/ToPCUIC/Stdlib/Strings.v @@ -1,5 +1,5 @@ Require Import Coq.Strings.String Coq.Strings.Ascii. -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. #[export] Instance quote_ascii : ground_quotable Ascii.ascii := (ltac:(induction 1; exact _)). #[export] Instance quote_string : ground_quotable string := (ltac:(induction 1; exact _)). diff --git a/quotation/theories/ToPCUIC/Coq/ssr.v b/quotation/theories/ToPCUIC/Stdlib/ssr.v similarity index 96% rename from quotation/theories/ToPCUIC/Coq/ssr.v rename to quotation/theories/ToPCUIC/Stdlib/ssr.v index db0a25f6a..ae1d3cf1a 100644 --- a/quotation/theories/ToPCUIC/Coq/ssr.v +++ b/quotation/theories/ToPCUIC/Stdlib/ssr.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From Coq.ssr Require Import ssrbool ssreflect. #[export] Instance quote_if_spec {A b vT vF} {not_b:Prop} {b' a} {qA : quotation_of A} {qvT : quotation_of vT} {qvF : quotation_of vF} {qnot_b : quotation_of not_b} {quote_not_b : ground_quotable not_b} : ground_quotable (@if_spec A b vT vF not_b b' a) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Utils/All_Forall.v b/quotation/theories/ToPCUIC/Utils/All_Forall.v index 0031d0442..a5f2dce70 100644 --- a/quotation/theories/ToPCUIC/Utils/All_Forall.v +++ b/quotation/theories/ToPCUIC/Utils/All_Forall.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init Coq.Lists. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init Stdlib.Lists. From MetaCoq.Utils Require Import All_Forall. #[export] Instance quote_All {A R ls} {qA : quotation_of A} {qR : quotation_of R} {quoteA : ground_quotable A} {quoteR : forall x, ground_quotable (R x)} : ground_quotable (@All A R ls) := ltac:(induction 1; exact _). diff --git a/quotation/theories/ToPCUIC/Utils/MCArith.v b/quotation/theories/ToPCUIC/Utils/MCArith.v index 418ee9300..bea31b9b4 100644 --- a/quotation/theories/ToPCUIC/Utils/MCArith.v +++ b/quotation/theories/ToPCUIC/Utils/MCArith.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCArith. #[export] Instance quote_BoolSpecSet {P Q : Prop} {b} {qP : quotation_of P} {qQ : quotation_of Q} {quoteP : ground_quotable P} {quoteQ : ground_quotable Q} : ground_quotable (BoolSpecSet P Q b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Utils/MCList.v b/quotation/theories/ToPCUIC/Utils/MCList.v index 17152944c..a2d9e372d 100644 --- a/quotation/theories/ToPCUIC/Utils/MCList.v +++ b/quotation/theories/ToPCUIC/Utils/MCList.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCList. #[export] Instance quote_nth_error_Spec {A l n o} {qA : quotation_of A} {quoteA : ground_quotable A} {qo : quotation_of o} {ql : quotation_of l} : ground_quotable (@nth_error_Spec A l n o) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Utils/MCOption.v b/quotation/theories/ToPCUIC/Utils/MCOption.v index ec961e3ba..0003efeee 100644 --- a/quotation/theories/ToPCUIC/Utils/MCOption.v +++ b/quotation/theories/ToPCUIC/Utils/MCOption.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCOption MCRelations. #[local] Hint Extern 0 => reflexivity : typeclass_instances. diff --git a/quotation/theories/ToPCUIC/Utils/MCProd.v b/quotation/theories/ToPCUIC/Utils/MCProd.v index 9d252cb1f..291466af7 100644 --- a/quotation/theories/ToPCUIC/Utils/MCProd.v +++ b/quotation/theories/ToPCUIC/Utils/MCProd.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCProd. Section and. diff --git a/quotation/theories/ToPCUIC/Utils/MCReflect.v b/quotation/theories/ToPCUIC/Utils/MCReflect.v index 5e3f01de4..270c9e0a7 100644 --- a/quotation/theories/ToPCUIC/Utils/MCReflect.v +++ b/quotation/theories/ToPCUIC/Utils/MCReflect.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCReflect. #[export] Instance quote_reflectT {A} {qA : quotation_of A} {quoteA : ground_quotable A} {quote_negA : ground_quotable (A -> False)} {b} : ground_quotable (@reflectT A b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToPCUIC/Utils/ReflectEq.v b/quotation/theories/ToPCUIC/Utils/ReflectEq.v index ddd2b0645..87b0bc8c6 100644 --- a/quotation/theories/ToPCUIC/Utils/ReflectEq.v +++ b/quotation/theories/ToPCUIC/Utils/ReflectEq.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import ReflectEq. #[export] Instance quote_reflectProp {A:Prop} {qA : quotation_of A} {quoteA : ground_quotable A} {quote_negA : ground_quotable (~A)} {b} : ground_quotable (@reflectProp A b). diff --git a/quotation/theories/ToPCUIC/Utils/bytestring.v b/quotation/theories/ToPCUIC/Utils/bytestring.v index 60f3e3cc3..6c6289d02 100644 --- a/quotation/theories/ToPCUIC/Utils/bytestring.v +++ b/quotation/theories/ToPCUIC/Utils/bytestring.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init. From MetaCoq.Utils Require Import bytestring. Module String. diff --git a/quotation/theories/ToPCUIC/Utils/utils.v b/quotation/theories/ToPCUIC/Utils/utils.v index 683155c2f..441ff944d 100644 --- a/quotation/theories/ToPCUIC/Utils/utils.v +++ b/quotation/theories/ToPCUIC/Utils/utils.v @@ -1,3 +1,3 @@ -From MetaCoq.Quotation.ToPCUIC Require Import Coq.Init Coq.Bool Coq.Numbers Coq.Lists. +From MetaCoq.Quotation.ToPCUIC Require Import Stdlib.Init Stdlib.Bool Stdlib.Numbers Stdlib.Lists. From MetaCoq.Quotation.ToPCUIC.Utils Require Import MCUtils monad_utils. From MetaCoq.Utils Require Import utils. diff --git a/quotation/theories/ToTemplate/Common/BasicAst.v b/quotation/theories/ToTemplate/Common/BasicAst.v index 81bf30b19..3c49b668d 100644 --- a/quotation/theories/ToTemplate/Common/BasicAst.v +++ b/quotation/theories/ToTemplate/Common/BasicAst.v @@ -1,5 +1,5 @@ From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Floats Coq.Numbers. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Floats Stdlib.Numbers. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) utils. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) Kernames. From MetaCoq.Common Require Import BasicAst. diff --git a/quotation/theories/ToTemplate/Common/Environment.v b/quotation/theories/ToTemplate/Common/Environment.v index 7494e89a3..f22f618b7 100644 --- a/quotation/theories/ToTemplate/Common/Environment.v +++ b/quotation/theories/ToTemplate/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.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.ssr utils BasicAst Primitive Universes Kernames. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.ssr utils BasicAst Primitive Universes Kernames. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) MCOption MCProd All_Forall. From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig. diff --git a/quotation/theories/ToTemplate/Common/EnvironmentTyping.v b/quotation/theories/ToTemplate/Common/EnvironmentTyping.v index bb7dc2708..2e4c657aa 100644 --- a/quotation/theories/ToTemplate/Common/EnvironmentTyping.v +++ b/quotation/theories/ToTemplate/Common/EnvironmentTyping.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import BasicAst Environment EnvironmentTyping Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Lists Coq.ssr. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.ssr. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) All_Forall MCOption. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) config BasicAst Kernames Universes Environment. From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig. diff --git a/quotation/theories/ToTemplate/Common/Kernames.v b/quotation/theories/ToTemplate/Common/Kernames.v index e7b51b711..38bd879f5 100644 --- a/quotation/theories/ToTemplate/Common/Kernames.v +++ b/quotation/theories/ToTemplate/Common/Kernames.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.MSets Coq.FSets bytestring. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.MSets Stdlib.FSets bytestring. From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Kernames.Instances. #[local] Hint Unfold ident qualid dirpath kername : quotation. diff --git a/quotation/theories/ToTemplate/Common/Primitive.v b/quotation/theories/ToTemplate/Common/Primitive.v index de30e8d71..fb43e1758 100644 --- a/quotation/theories/ToTemplate/Common/Primitive.v +++ b/quotation/theories/ToTemplate/Common/Primitive.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Common Require Import Primitive. #[export] Instance quote_prim_tag : ground_quotable prim_tag := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Common/Universes.v b/quotation/theories/ToTemplate/Common/Universes.v index bf1ad2912..3cd0bcde9 100644 --- a/quotation/theories/ToTemplate/Common/Universes.v +++ b/quotation/theories/ToTemplate/Common/Universes.v @@ -1,5 +1,5 @@ From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.Coq Require Import (hints) Init MSets Numbers. +From MetaCoq.Quotation.ToTemplate.Stdlib Require Import (hints) Init MSets Numbers. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) MCOption bytestring. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) BasicAst config. From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Universes.Instances. diff --git a/quotation/theories/ToTemplate/Common/config.v b/quotation/theories/ToTemplate/Common/config.v index 7a4182d0f..a92904ea8 100644 --- a/quotation/theories/ToTemplate/Common/config.v +++ b/quotation/theories/ToTemplate/Common/config.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Common Require Import config. #[export] Instance quote_checker_flags : ground_quotable checker_flags := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Equations.v b/quotation/theories/ToTemplate/Equations.v index 3a2d83815..d69e72001 100644 --- a/quotation/theories/ToTemplate/Equations.v +++ b/quotation/theories/ToTemplate/Equations.v @@ -1,5 +1,5 @@ From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init. From Equations Require Import Init. Local Set Universe Polymorphism. diff --git a/quotation/theories/ToTemplate/Equations/Type.v b/quotation/theories/ToTemplate/Equations/Type.v index 3c5efd12e..8e486a3e3 100644 --- a/quotation/theories/ToTemplate/Equations/Type.v +++ b/quotation/theories/ToTemplate/Equations/Type.v @@ -1,5 +1,5 @@ From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Equations. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Equations. Set Warnings "-notation-overridden". From Equations.Type Require Import Logic Relation. Set Warnings "notation-overridden". diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v index b0f730bc3..d469ddf85 100644 --- a/quotation/theories/ToTemplate/Init.v +++ b/quotation/theories/ToTemplate/Init.v @@ -4,7 +4,7 @@ From MetaCoq.Common Require Import MonadBasicAst. From MetaCoq.Template Require Import MonadAst TemplateMonad Ast Loader. From MetaCoq.Quotation Require Export CommonUtils. Require Import Equations.Prop.Classes. -Require Import Coq.Lists.List. +Require Import Stdlib.Lists.List. Export TemplateMonad.Common (export, local, global). Import ListNotations. @@ -612,5 +612,5 @@ Global Arguments tmDeclareQuotationOfModule {_%_bool} _ _ _%_bs. (* Require Import MSetPositive. Instance: debug_opt := true. -MetaCoq Run (tmMakeQuotationOfModule None "Coq.MSets.MSetPositive.PositiveSet"%bs). +MetaCoq Run (tmMakeQuotationOfModule None "Stdlib.MSets.MSetPositive.PositiveSet"%bs). *) diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.v index 259ad02fb..d8aadab3f 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.v index 3db1cd993..50d709100 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapAVL.Sig FMapList.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.FSets Require Import FMapAVL.Sig FMapList.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.v index 15fe993b4..944b47e4f 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.FSets Require Import FMapFacts.Sig. Module qKernameMapFact. Module qF <: QuotationOfWFacts_fun Kername.OT KernameMap KernameMapFact.F. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.v index 0c3b58576..bae0c9750 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qKernameSet <: MSetAVL.QuotationOfMake Kername KernameSet. MetaCoq Run (tmMakeQuotationOfModule everything None "KernameSet"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v index 45e03bdbe..cfdc015d3 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Kernames. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.v index 2c85d2ebe..43960a281 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qConstraintSet <: MSetAVL.QuotationOfMake UnivConstraint ConstraintSet. MetaCoq Run (tmMakeQuotationOfModule everything None "ConstraintSet"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v index 8e77b0d2c..09302c29a 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/Level/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/Level/Instances.v index 40de3ec6c..07343e6f8 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/Level/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/Level/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.v index 527d205ab..39e646000 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.v index 1dcbc18c9..aab6e725d 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetList.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetList.Sig. Module qLevelExprSet <: MSetList.QuotationOfMakeWithLeibniz LevelExpr LevelExprSet. MetaCoq Run (tmMakeQuotationOfModule everything None "LevelExprSet"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v index 0ace7b49e..dc76a09e1 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.v index f2f8fe104..4e7dbbd41 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetAVL.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetAVL.Sig. Module qLevelSet <: MSetAVL.QuotationOfMake Level LevelSet. MetaCoq Run (tmMakeQuotationOfModule everything None "LevelSet"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v index 91696d248..9d4787251 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetProperties.Sig MSetDecide.Sig MSetFacts.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v index 775965a56..fd54c472f 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v @@ -1,6 +1,6 @@ From MetaCoq.Common Require Import Universes. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v similarity index 85% rename from quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v index d48e39b7c..d1fad9785 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapAVL/Sig.v @@ -2,8 +2,8 @@ From Coq.FSets Require Import FMapAVL. From Coq.Structures Require Import Equalities OrdersAlt. From MetaCoq.Utils Require Import MCFSets. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapList.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.FSets Require Import FMapList.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapFacts/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapInterface/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapList/Sig.v similarity index 87% rename from quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapList/Sig.v index c70865efb..838412296 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/FSets/FMapList/Sig.v @@ -2,7 +2,7 @@ From Coq.FSets Require Import FMapList. From Coq.Structures Require Import Equalities OrdersAlt. From MetaCoq.Utils Require Import MCFSets. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetAVL/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetDecide/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetFacts/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetInterface/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetList/Sig.v similarity index 92% rename from quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetList/Sig.v index a17499f73..e2b481d6d 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetList/Sig.v @@ -2,7 +2,7 @@ From Coq.Structures Require Import Equalities Orders. From Coq.MSets Require Import MSetList. From MetaCoq.Utils Require Import MCMSets. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetInterface.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetInterface.Sig. Module Type QuotationOfOrderedTypeWithLeibniz (O : OrderedTypeWithLeibniz). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "O"). diff --git a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v similarity index 82% rename from quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v index a97211a1d..23afa330d 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/MSets/MSetProperties/Sig.v @@ -1,8 +1,8 @@ From Coq.MSets Require Import MSetProperties. From MetaCoq.Utils Require Import MCMSets. -From MetaCoq.Quotation.ToPCUIC Require Import Init. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.Structures Require Import OrdersFacts.Sig. -From MetaCoq.Quotation.ToPCUIC.QuotationOf.Coq.MSets Require Import MSetFacts.Sig MSetDecide.Sig. +From MetaCoq.Quotation.ToTemplate Require Import Init. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import OrdersFacts.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetFacts.Sig MSetDecide.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/Equalities/Sig.v similarity index 100% rename from quotation/theories/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/Equalities/Sig.v diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/Orders/Sig.v similarity index 99% rename from quotation/theories/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/Orders/Sig.v index c1e91e9a4..09ff67976 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/Orders/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Orders. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq Require Export Structures.Equalities.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib Require Export Structures.Equalities.Sig. Module Type QuotationOfHasLt (Import T : Typ) (Import E : HasLt T). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "E"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v similarity index 98% rename from quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v index c315e1a41..96bb694cb 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersAlt/Sig.v @@ -1,7 +1,7 @@ From Coq.Structures Require Import Equalities OrdersAlt. From Coq.Structures Require OrderedType. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Import List.ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v similarity index 97% rename from quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v index 006a5bec7..5ea261908 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersFacts/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Equalities Orders OrdersFacts. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Module Type QuotationOfCompareFacts (O : DecStrOrder) (F : CompareFacts O). MetaCoq Run (tmDeclareQuotationOfModule everything (Some export) "F"). diff --git a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v similarity index 94% rename from quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.v rename to quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v index b7db44a04..ea617b8bb 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Stdlib/Structures/OrdersTac/Sig.v @@ -1,6 +1,6 @@ From Coq.Structures Require Import Equalities Orders OrdersTac. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq Require Export Structures.Orders.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib Require Export Structures.Orders.Sig. Module Type QuotationOfIsTotalOrder (O : EqLtLe) (S : IsTotalOrder O) := QuotationOfIsEq O S <+ QuotationOfIsStrOrder O S <+ QuotationOfLeIsLtEq O S <+ QuotationOfLtIsTotal O S. diff --git a/quotation/theories/ToTemplate/Coq/Bool.v b/quotation/theories/ToTemplate/Stdlib/Bool.v similarity index 88% rename from quotation/theories/ToTemplate/Coq/Bool.v rename to quotation/theories/ToTemplate/Stdlib/Bool.v index c98868e31..46f477169 100644 --- a/quotation/theories/ToTemplate/Coq/Bool.v +++ b/quotation/theories/ToTemplate/Stdlib/Bool.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From Coq.Bool Require Import Bool IfProp. #[export] Instance quote_reflect {P : Prop} {qP : quotation_of P} {quoteP : ground_quotable P} {quote_negP : ground_quotable (~P)} {b} : ground_quotable (reflect P b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Coq/FSets.v b/quotation/theories/ToTemplate/Stdlib/FSets.v similarity index 93% rename from quotation/theories/ToTemplate/Coq/FSets.v rename to quotation/theories/ToTemplate/Stdlib/FSets.v index 3e410c4c2..448ed52b4 100644 --- a/quotation/theories/ToTemplate/Coq/FSets.v +++ b/quotation/theories/ToTemplate/Stdlib/FSets.v @@ -1,9 +1,9 @@ From Coq Require Import Structures.Equalities Structures.OrdersAlt FMapInterface FMapList FMapAVL FMapFullAVL FMapFacts. From MetaCoq.Utils Require Import MCUtils MCFSets. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Numbers Coq.Init Coq.Lists. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import OrdersAlt.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.FSets Require Import FMapInterface.Sig FMapFacts.Sig FMapAVL.Sig FMapList.Sig. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Numbers Stdlib.Init Stdlib.Lists. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import OrdersAlt.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.FSets Require Import FMapInterface.Sig FMapFacts.Sig FMapAVL.Sig FMapList.Sig. From MetaCoq.Quotation.ToTemplate.QuotationOf.Utils Require Import MCFSets.Sig. #[export] Hint Unfold Int.Z_as_Int.t : quotation. diff --git a/quotation/theories/ToTemplate/Coq/Floats.v b/quotation/theories/ToTemplate/Stdlib/Floats.v similarity index 90% rename from quotation/theories/ToTemplate/Coq/Floats.v rename to quotation/theories/ToTemplate/Stdlib/Floats.v index 85d7002f1..3c95e730c 100644 --- a/quotation/theories/ToTemplate/Coq/Floats.v +++ b/quotation/theories/ToTemplate/Stdlib/Floats.v @@ -1,6 +1,6 @@ From Coq.Floats Require Import FloatClass Floats PrimFloat SpecFloat. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Numbers. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Numbers. #[export] Instance quote_float : ground_quotable float := fun f => Ast.tFloat f. #[export] Instance quote_float_class : ground_quotable float_class := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Coq/Init.v b/quotation/theories/ToTemplate/Stdlib/Init.v similarity index 100% rename from quotation/theories/ToTemplate/Coq/Init.v rename to quotation/theories/ToTemplate/Stdlib/Init.v diff --git a/quotation/theories/ToTemplate/Coq/Lists.v b/quotation/theories/ToTemplate/Stdlib/Lists.v similarity index 98% rename from quotation/theories/ToTemplate/Coq/Lists.v rename to quotation/theories/ToTemplate/Stdlib/Lists.v index a360203e4..1eda7a122 100644 --- a/quotation/theories/ToTemplate/Coq/Lists.v +++ b/quotation/theories/ToTemplate/Stdlib/Lists.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List. Require Import Coq.Lists.ListDec. From MetaCoq.Utils Require Import ReflectEq. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init. From Equations.Prop Require Import Classes. Import ListNotations. Local Open Scope list_scope. diff --git a/quotation/theories/ToTemplate/Coq/MSets.v b/quotation/theories/ToTemplate/Stdlib/MSets.v similarity index 97% rename from quotation/theories/ToTemplate/Coq/MSets.v rename to quotation/theories/ToTemplate/Stdlib/MSets.v index 0458adaf5..e0676267b 100644 --- a/quotation/theories/ToTemplate/Coq/MSets.v +++ b/quotation/theories/ToTemplate/Stdlib/MSets.v @@ -1,9 +1,9 @@ From Coq Require Import MSetInterface MSetList MSetAVL MSetFacts MSetProperties MSetDecide. From MetaCoq.Utils Require Import MCMSets. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Numbers Coq.Init Coq.Lists. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.Structures Require Import Orders.Sig. -From MetaCoq.Quotation.ToTemplate.QuotationOf.Coq.MSets Require Import MSetInterface.Sig MSetProperties.Sig MSetAVL.Sig MSetList.Sig. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Numbers Stdlib.Init Stdlib.Lists. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.Structures Require Import Orders.Sig. +From MetaCoq.Quotation.ToTemplate.QuotationOf.Stdlib.MSets Require Import MSetInterface.Sig MSetProperties.Sig MSetAVL.Sig MSetList.Sig. From MetaCoq.Quotation.ToTemplate.QuotationOf.Utils Require Import MCMSets.Sig. #[export] Hint Unfold Int.Z_as_Int.t : quotation. diff --git a/quotation/theories/ToTemplate/Coq/Numbers.v b/quotation/theories/ToTemplate/Stdlib/Numbers.v similarity index 96% rename from quotation/theories/ToTemplate/Coq/Numbers.v rename to quotation/theories/ToTemplate/Stdlib/Numbers.v index ce17ecff9..89fb4b9c6 100644 --- a/quotation/theories/ToTemplate/Coq/Numbers.v +++ b/quotation/theories/ToTemplate/Stdlib/Numbers.v @@ -5,7 +5,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts Cyclic.Abstract.CarryType . From Coq Require Import ZArith. -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. #[export] Instance quote_positive : ground_quotable positive := ltac:(induction 1; exact _). #[export] Instance quote_N : ground_quotable N := ltac:(induction 1; exact _). diff --git a/quotation/theories/ToTemplate/Coq/Strings.v b/quotation/theories/ToTemplate/Stdlib/Strings.v similarity index 79% rename from quotation/theories/ToTemplate/Coq/Strings.v rename to quotation/theories/ToTemplate/Stdlib/Strings.v index b947ea986..b7e68b141 100644 --- a/quotation/theories/ToTemplate/Coq/Strings.v +++ b/quotation/theories/ToTemplate/Stdlib/Strings.v @@ -1,5 +1,5 @@ Require Import Coq.Strings.String Coq.Strings.Ascii. -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. #[export] Instance quote_ascii : ground_quotable Ascii.ascii := (ltac:(induction 1; exact _)). #[export] Instance quote_string : ground_quotable string := (ltac:(induction 1; exact _)). diff --git a/quotation/theories/ToTemplate/Coq/ssr.v b/quotation/theories/ToTemplate/Stdlib/ssr.v similarity index 96% rename from quotation/theories/ToTemplate/Coq/ssr.v rename to quotation/theories/ToTemplate/Stdlib/ssr.v index ee4b6a62b..ea05b511a 100644 --- a/quotation/theories/ToTemplate/Coq/ssr.v +++ b/quotation/theories/ToTemplate/Stdlib/ssr.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From Coq.ssr Require Import ssrbool ssreflect. #[export] Instance quote_if_spec {A b vT vF} {not_b:Prop} {b' a} {qA : quotation_of A} {qvT : quotation_of vT} {qvF : quotation_of vF} {qnot_b : quotation_of not_b} {quote_not_b : ground_quotable not_b} : ground_quotable (@if_spec A b vT vF not_b b' a) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Template/Ast.v b/quotation/theories/ToTemplate/Template/Ast.v index 925d6c009..16feae796 100644 --- a/quotation/theories/ToTemplate/Template/Ast.v +++ b/quotation/theories/ToTemplate/Template/Ast.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import Ast ReflectAst Induction. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) Universes BasicAst Kernames. From MetaCoq.Quotation.ToTemplate.Common Require Import Environment EnvironmentTyping. From MetaCoq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig. diff --git a/quotation/theories/ToTemplate/Template/AstUtils.v b/quotation/theories/ToTemplate/Template/AstUtils.v index d877facb1..670618504 100644 --- a/quotation/theories/ToTemplate/Template/AstUtils.v +++ b/quotation/theories/ToTemplate/Template/AstUtils.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import AstUtils. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init. From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast. #[export] Instance quote_mkApps_spec {f args fargs1 args2 fargs} : ground_quotable (@mkApps_spec f args fargs1 args2 fargs) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Template/TermEquality.v b/quotation/theories/ToTemplate/Template/TermEquality.v index fdbc90d07..f448b7ee4 100644 --- a/quotation/theories/ToTemplate/Template/TermEquality.v +++ b/quotation/theories/ToTemplate/Template/TermEquality.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import Ast TermEquality. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) utils All_Forall. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) config Reflect Environment Universes BasicAst Kernames. From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast AstUtils Induction. @@ -20,7 +20,7 @@ Section with_R. #[export] Instance quote_cmp_opt_variance {pb v u u'} (subr : RelationClasses.subrelation (cmp_universe Conv) (cmp_universe pb)) : ground_quotable (@cmp_opt_variance cmp_universe pb v u u'). Proof using cmp_universe qRe quoteRe. destruct v; cbv [cmp_opt_variance]; try exact _. - eapply Coq.Init.quote_or_dec; try exact _. + eapply Stdlib.Init.quote_or_dec; try exact _. now apply cmp_opt_variance_var_dec. Defined. diff --git a/quotation/theories/ToTemplate/Template/Typing.v b/quotation/theories/ToTemplate/Template/Typing.v index dc1da98a6..fce61e22a 100644 --- a/quotation/theories/ToTemplate/Template/Typing.v +++ b/quotation/theories/ToTemplate/Template/Typing.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import Ast Typing. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) utils All_Forall (* MCProd*). From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) config BasicAst Universes Kernames Environment EnvironmentTyping Primitive Reflect. From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) AstUtils diff --git a/quotation/theories/ToTemplate/Template/TypingWf.v b/quotation/theories/ToTemplate/Template/TypingWf.v index 0ca45b7c4..7948ec05d 100644 --- a/quotation/theories/ToTemplate/Template/TypingWf.v +++ b/quotation/theories/ToTemplate/Template/TypingWf.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import TypingWf. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) All_Forall. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) BasicAst. From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast WfAst. diff --git a/quotation/theories/ToTemplate/Template/WfAst.v b/quotation/theories/ToTemplate/Template/WfAst.v index 41c72d916..30333c78e 100644 --- a/quotation/theories/ToTemplate/Template/WfAst.v +++ b/quotation/theories/ToTemplate/Template/WfAst.v @@ -1,6 +1,6 @@ From MetaCoq.Template Require Import Ast WfAst. From MetaCoq.Quotation.ToTemplate Require Import Init. -From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init Coq.Lists Coq.Numbers Coq.Floats. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Stdlib.Init Stdlib.Lists Stdlib.Numbers Stdlib.Floats. From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) utils All_Forall MCProd MCOption. From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) config BasicAst Universes Kernames. From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast AstUtils Induction UnivSubst. diff --git a/quotation/theories/ToTemplate/Utils/All_Forall.v b/quotation/theories/ToTemplate/Utils/All_Forall.v index 9fbe15c9f..d7163a67c 100644 --- a/quotation/theories/ToTemplate/Utils/All_Forall.v +++ b/quotation/theories/ToTemplate/Utils/All_Forall.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init Coq.Lists. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init Stdlib.Lists. From MetaCoq.Utils Require Import All_Forall. #[export] Instance quote_All {A R ls} {qA : quotation_of A} {qR : quotation_of R} {quoteA : ground_quotable A} {quoteR : forall x, ground_quotable (R x)} : ground_quotable (@All A R ls) := ltac:(induction 1; exact _). diff --git a/quotation/theories/ToTemplate/Utils/MCArith.v b/quotation/theories/ToTemplate/Utils/MCArith.v index c5eca7cfc..bcc3ad9b9 100644 --- a/quotation/theories/ToTemplate/Utils/MCArith.v +++ b/quotation/theories/ToTemplate/Utils/MCArith.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCArith. #[export] Instance quote_BoolSpecSet {P Q : Prop} {b} {qP : quotation_of P} {qQ : quotation_of Q} {quoteP : ground_quotable P} {quoteQ : ground_quotable Q} : ground_quotable (BoolSpecSet P Q b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Utils/MCList.v b/quotation/theories/ToTemplate/Utils/MCList.v index 53728f9b6..2e5415404 100644 --- a/quotation/theories/ToTemplate/Utils/MCList.v +++ b/quotation/theories/ToTemplate/Utils/MCList.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCList. #[export] Instance quote_nth_error_Spec {A l n o} {qA : quotation_of A} {quoteA : ground_quotable A} {qo : quotation_of o} {ql : quotation_of l} : ground_quotable (@nth_error_Spec A l n o) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Utils/MCOption.v b/quotation/theories/ToTemplate/Utils/MCOption.v index 6d5a37cf0..d675d77ed 100644 --- a/quotation/theories/ToTemplate/Utils/MCOption.v +++ b/quotation/theories/ToTemplate/Utils/MCOption.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCOption MCRelations. #[local] Hint Extern 0 => reflexivity : typeclass_instances. diff --git a/quotation/theories/ToTemplate/Utils/MCProd.v b/quotation/theories/ToTemplate/Utils/MCProd.v index 4e85411d9..ca495b4c8 100644 --- a/quotation/theories/ToTemplate/Utils/MCProd.v +++ b/quotation/theories/ToTemplate/Utils/MCProd.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCProd. Section and. diff --git a/quotation/theories/ToTemplate/Utils/MCReflect.v b/quotation/theories/ToTemplate/Utils/MCReflect.v index dc3c77035..1735990cb 100644 --- a/quotation/theories/ToTemplate/Utils/MCReflect.v +++ b/quotation/theories/ToTemplate/Utils/MCReflect.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import MCReflect. #[export] Instance quote_reflectT {A} {qA : quotation_of A} {quoteA : ground_quotable A} {quote_negA : ground_quotable (A -> False)} {b} : ground_quotable (@reflectT A b) := ltac:(destruct 1; exact _). diff --git a/quotation/theories/ToTemplate/Utils/ReflectEq.v b/quotation/theories/ToTemplate/Utils/ReflectEq.v index 24c1f69fa..bca278364 100644 --- a/quotation/theories/ToTemplate/Utils/ReflectEq.v +++ b/quotation/theories/ToTemplate/Utils/ReflectEq.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import ReflectEq. #[export] Instance quote_reflectProp {A:Prop} {qA : quotation_of A} {quoteA : ground_quotable A} {quote_negA : ground_quotable (~A)} {b} : ground_quotable (@reflectProp A b). diff --git a/quotation/theories/ToTemplate/Utils/bytestring.v b/quotation/theories/ToTemplate/Utils/bytestring.v index bd0ba88e4..341748595 100644 --- a/quotation/theories/ToTemplate/Utils/bytestring.v +++ b/quotation/theories/ToTemplate/Utils/bytestring.v @@ -1,4 +1,4 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. From MetaCoq.Utils Require Import bytestring. Module String. diff --git a/quotation/theories/ToTemplate/Utils/utils.v b/quotation/theories/ToTemplate/Utils/utils.v index 381dc1fc1..7155e9949 100644 --- a/quotation/theories/ToTemplate/Utils/utils.v +++ b/quotation/theories/ToTemplate/Utils/utils.v @@ -1,3 +1,3 @@ -From MetaCoq.Quotation.ToTemplate Require Import Coq.Init Coq.Bool Coq.Numbers Coq.Lists. +From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init Stdlib.Bool Stdlib.Numbers Stdlib.Lists. From MetaCoq.Quotation.ToTemplate.Utils Require Import MCUtils monad_utils. From MetaCoq.Utils Require Import utils. diff --git a/safechecker-plugin/theories/Extraction.v b/safechecker-plugin/theories/Extraction.v index 2e7c0d86d..00a677373 100644 --- a/safechecker-plugin/theories/Extraction.v +++ b/safechecker-plugin/theories/Extraction.v @@ -1,5 +1,5 @@ (* Distributed under the terms of the MIT license. *) -From Coq Require Import OrdersTac Ascii ExtrOcamlBasic ExtrOCamlInt63 ExtrOCamlFloats. +From Stdlib Require Import OrdersTac Ascii ExtrOcamlBasic ExtrOCamlInt63 ExtrOCamlFloats. From MetaCoq.Utils Require Import utils. From MetaCoq.SafeChecker Require Import PCUICWfEnvImpl PCUICSafeChecker PCUICSafeConversion. From MetaCoq.SafeCheckerPlugin Require Import SafeTemplateChecker. @@ -51,4 +51,4 @@ Definition infer_and_print_template_program_with_guard {cf} {nor} := Separate Extraction MakeOrderTac PCUICSafeChecker.typecheck_program infer_and_print_template_program_with_guard (* The following directives ensure separate extraction does not produce name clashes *) - Coq.Strings.String UnivSubst PCUICPretty. + Stdlib.Strings.String UnivSubst PCUICPretty. diff --git a/safechecker/theories/PCUICSafeChecker.v b/safechecker/theories/PCUICSafeChecker.v index 4a32dfd3f..48cf5a26a 100644 --- a/safechecker/theories/PCUICSafeChecker.v +++ b/safechecker/theories/PCUICSafeChecker.v @@ -106,7 +106,7 @@ Definition gcs_equal x y : Prop := (** It otherwise tries [auto with *], very bad idea. *) -Ltac Coq.Program.Tactics.program_solve_wf ::= +Ltac Stdlib.Program.Tactics.program_solve_wf ::= match goal with | |- @Wf.well_founded _ _ => auto with subterm wf | |- ?T => match type of T with diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v index 336896377..68cbe06d2 100644 --- a/safechecker/theories/PCUICTypeChecker.v +++ b/safechecker/theories/PCUICTypeChecker.v @@ -25,7 +25,7 @@ From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICSafeReduce PCUICEr From Equations Require Import Equations. Require Import ssreflect ssrbool. -Require Import Coq.Program.Program. +Require Import Stdlib.Program.Program. Local Set Keyed Unification. Set Equations Transparent. @@ -125,7 +125,7 @@ Proof. Qed. (** It otherwise tries [auto with *], very bad idea. *) -Ltac Coq.Program.Tactics.program_solve_wf ::= +Ltac Stdlib.Program.Tactics.program_solve_wf ::= match goal with | |- @Wf.well_founded _ _ => auto with subterm wf | |- ?T => match type of T with diff --git a/template-coq/theories/Constants.v b/template-coq/theories/Constants.v index 62c1a06a7..a8ea5dd3e 100644 --- a/template-coq/theories/Constants.v +++ b/template-coq/theories/Constants.v @@ -9,49 +9,49 @@ Register bytestring.String.t as metacoq.string.type. Register bytestring.String.EmptyString as metacoq.string.nil. Register bytestring.String.String as metacoq.string.cons. -Register Coq.Init.Byte.byte as metacoq.byte.type. +Register Stdlib.Init.Byte.byte as metacoq.byte.type. -Register Coq.Init.Datatypes.nat as metacoq.nat.type. -Register Coq.Init.Datatypes.O as metacoq.nat.zero. -Register Coq.Init.Datatypes.S as metacoq.nat.succ. +Register Stdlib.Init.Datatypes.nat as metacoq.nat.type. +Register Stdlib.Init.Datatypes.O as metacoq.nat.zero. +Register Stdlib.Init.Datatypes.S as metacoq.nat.succ. -Register Coq.Init.Datatypes.bool as metacoq.bool.type. -Register Coq.Init.Datatypes.true as metacoq.bool.true. -Register Coq.Init.Datatypes.false as metacoq.bool.false. +Register Stdlib.Init.Datatypes.bool as metacoq.bool.type. +Register Stdlib.Init.Datatypes.true as metacoq.bool.true. +Register Stdlib.Init.Datatypes.false as metacoq.bool.false. -Register Coq.Init.Datatypes.option as metacoq.option.type. -Register Coq.Init.Datatypes.None as metacoq.option.none. -Register Coq.Init.Datatypes.Some as metacoq.option.some. +Register Stdlib.Init.Datatypes.option as metacoq.option.type. +Register Stdlib.Init.Datatypes.None as metacoq.option.none. +Register Stdlib.Init.Datatypes.Some as metacoq.option.some. Register MetaCoq.Template.TemplateMonad.Common.my_None as metacoq.option_instance.none. Register MetaCoq.Template.TemplateMonad.Common.my_Some as metacoq.option_instance.some. -Register Coq.Init.Datatypes.list as metacoq.list.type. -Register Coq.Init.Datatypes.nil as metacoq.list.nil. -Register Coq.Init.Datatypes.cons as metacoq.list.cons. +Register Stdlib.Init.Datatypes.list as metacoq.list.type. +Register Stdlib.Init.Datatypes.nil as metacoq.list.nil. +Register Stdlib.Init.Datatypes.cons as metacoq.list.cons. -Register Coq.Init.Datatypes.prod as metacoq.prod.type. -Register Coq.Init.Datatypes.pair as metacoq.prod.intro. +Register Stdlib.Init.Datatypes.prod as metacoq.prod.type. +Register Stdlib.Init.Datatypes.pair as metacoq.prod.intro. -Register Coq.Init.Datatypes.sum as metacoq.sum.type. -Register Coq.Init.Datatypes.inl as metacoq.sum.inl. -Register Coq.Init.Datatypes.inr as metacoq.sum.inr. +Register Stdlib.Init.Datatypes.sum as metacoq.sum.type. +Register Stdlib.Init.Datatypes.inl as metacoq.sum.inl. +Register Stdlib.Init.Datatypes.inr as metacoq.sum.inr. -Register Coq.Init.Datatypes.unit as metacoq.unit.type. -Register Coq.Init.Datatypes.tt as metacoq.unit.intro. +Register Stdlib.Init.Datatypes.unit as metacoq.unit.type. +Register Stdlib.Init.Datatypes.tt as metacoq.unit.intro. -Register Coq.Init.Specif.sigT as metacoq.sigma.type. -Register Coq.Init.Specif.existT as metacoq.sigma.intro. +Register Stdlib.Init.Specif.sigT as metacoq.sigma.type. +Register Stdlib.Init.Specif.existT as metacoq.sigma.intro. Register MetaCoq.Template.TemplateMonad.Common.existT_typed_term as metacoq.sigma.typed_term. -Register Coq.Numbers.BinNums.positive as metacoq.pos.type. -Register Coq.Numbers.BinNums.xI as metacoq.pos.xI. -Register Coq.Numbers.BinNums.xO as metacoq.pos.xO. -Register Coq.Numbers.BinNums.xH as metacoq.pos.xH. +Register Stdlib.Numbers.BinNums.positive as metacoq.pos.type. +Register Stdlib.Numbers.BinNums.xI as metacoq.pos.xI. +Register Stdlib.Numbers.BinNums.xO as metacoq.pos.xO. +Register Stdlib.Numbers.BinNums.xH as metacoq.pos.xH. -Register Coq.Numbers.BinNums.Z as metacoq.Z.type. -Register Coq.Numbers.BinNums.Zpos as metacoq.Z.pos. -Register Coq.Numbers.BinNums.Zneg as metacoq.Z.neg. -Register Coq.Numbers.BinNums.Z0 as metacoq.Z.zero. +Register Stdlib.Numbers.BinNums.Z as metacoq.Z.type. +Register Stdlib.Numbers.BinNums.Zpos as metacoq.Z.pos. +Register Stdlib.Numbers.BinNums.Zneg as metacoq.Z.neg. +Register Stdlib.Numbers.BinNums.Z0 as metacoq.Z.zero. (* Ast *) Register MetaCoq.Common.BasicAst.relevance as metacoq.ast.relevance. diff --git a/test-suite/erasure_test.v b/test-suite/erasure_test.v index ddea7abab..f966b28ed 100644 --- a/test-suite/erasure_test.v +++ b/test-suite/erasure_test.v @@ -7,16 +7,16 @@ MetaCoq Erase -help. MetaCoq Erase nat. (* -Environment is well-formed and Ind(Coq.Init.Datatypes.nat,0,[]) has type: ⧆ +Environment is well-formed and Ind(Stdlib.Init.Datatypes.nat,0,[]) has type: ⧆ *) MetaCoq Erase I. MetaCoq Erase true. (* -Environment is well-formed and Construct(Coq.Init.Logic.True,0,0,[]) erases to: +Environment is well-formed and Construct(Stdlib.Init.Logic.True,0,0,[]) erases to: ⧆ -Environment is well-formed and Construct(Coq.Init.Datatypes.bool,0,0,[]) erases to: -Construct(Coq.Init.Datatypes.bool,0,0) +Environment is well-formed and Construct(Stdlib.Init.Datatypes.bool,0,0,[]) erases to: +Construct(Stdlib.Init.Datatypes.bool,0,0) *) MetaCoq Erase (exist (fun x => x = 0) 0 (eq_refl)). @@ -26,7 +26,7 @@ Definition test := (proj1_sig (exist (fun x => x = 0) 0 (eq_refl))). MetaCoq Erase -typed test. (** Cofix *) -From Coq Require Import StreamMemo. +From Stdlib Require Import StreamMemo. MetaCoq Quote Recursively Definition memo := memo_make. diff --git a/test-suite/extractable.v b/test-suite/extractable.v index bfde3e025..e985c583a 100644 --- a/test-suite/extractable.v +++ b/test-suite/extractable.v @@ -50,7 +50,7 @@ Print blah0. MetaCoq Test Quote nat. MetaCoq Run - (tmBind (tmQuoteInductive (MPfile ["Datatypes"; "Init"; "Coq"], "nat")) + (tmBind (tmQuoteInductive (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat")) (fun mi => tmMsg (string_of_nat (length mi.(ind_bodies))))). Definition nAnon := {| binder_name := nAnon; binder_relevance := Relevant |}. @@ -77,6 +77,6 @@ MetaCoq Run (fun s => tmMsg (string_of_modpath s))). MetaCoq Test Quote plus. -MetaCoq Run (tmQuoteInductive (MPfile ["Datatypes"; "Init"; "Coq"], "nat")). +MetaCoq Run (tmQuoteInductive (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat")). -MetaCoq Run (tmQuoteConstant (MPfile ["Nat"; "Init"; "Coq"], "add") true). +MetaCoq Run (tmQuoteConstant (MPfile ["Nat"; "Init"; "Stdlib"], "add") true). diff --git a/test-suite/modules_sections.v b/test-suite/modules_sections.v index c8d82272b..131c4ecf1 100644 --- a/test-suite/modules_sections.v +++ b/test-suite/modules_sections.v @@ -79,9 +79,9 @@ MetaCoq Run (bc <- tmQuote S.b ;; MetaCoq Test Quote my_projT2. MetaCoq Test Unquote - (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 0 []). + (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []). MetaCoq Unquote Definition zero_from_syntax - := (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 0 []). + := (Ast.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0) 0 []). Existing Class nat. @@ -111,5 +111,5 @@ MetaCoq Run (tmLocateModule1 "B" >>= tmPrint). MetaCoq Run (tmLocateModule1 "S" >>= tmPrint). MetaCoq Run (tmLocateModType1 "X" >>= tmPrint). Fail MetaCoq Run (tmLocateModType1 "B" >>= tmPrint). -Fail MetaCoq Run (tmLocateModType1 "modules_sections.S" >>= tmPrint). (* finds (MPdot (MPfile ["FMapInterface"; "FSets"; "Coq"]) "S") if unqualified *) +Fail MetaCoq Run (tmLocateModType1 "modules_sections.S" >>= tmPrint). (* finds (MPdot (MPfile ["FMapInterface"; "FSets"; "Stdlib"]) "S") if unqualified *) Fail MetaCoq Run (tmLocateModule1 "X" >>= tmPrint). diff --git a/test-suite/proj.v b/test-suite/proj.v index 0273b99b5..61b862ace 100644 --- a/test-suite/proj.v +++ b/test-suite/proj.v @@ -43,8 +43,8 @@ Import ListNotations. Definition qprod' := mkInd (MPfile ["proj"; "TestSuite"; "MetaCoq"], "prod'") 0. -Definition qnat := mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0. -Definition qbool := mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "bool") 0. +Definition qnat := mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "nat") 0. +Definition qbool := mkInd (MPfile ["Datatypes"; "Init"; "Stdlib"], "bool") 0. MetaCoq Unquote Definition x := (tProj (mkProjection qprod' 2 1) (tApp (tConstruct qprod' 0 nil) diff --git a/test-suite/safechecker_test.v b/test-suite/safechecker_test.v index a506cd694..542cec8e2 100644 --- a/test-suite/safechecker_test.v +++ b/test-suite/safechecker_test.v @@ -6,7 +6,7 @@ Local Open Scope string_scope. MetaCoq SafeCheck nat. (* -Environment is well-formed and Ind(Coq.Init.Datatypes.nat,0,[]) has type: Sort([Set]) +Environment is well-formed and Ind(Stdlib.Init.Datatypes.nat,0,[]) has type: Sort([Set]) *) MetaCoq SafeCheck (3 + 1). @@ -18,13 +18,13 @@ MetaCoq CoqCheck bool_list. (* Time MetaCoq SafeCheck @infer_and_print_template_program. *) (* Uses template polymorphism: Error: -Type error: Terms are not <= for cumulativity: Sort([Coq.Init.Datatypes.23,Coq.Init.Datatypes.24]) Sort([Set]) after reduction: Sort([Coq.Init.Datatypes.23,Coq.Init.Datatypes.24]) Sort([Set]), while checking MetaCoq.Template.Universes.Universe.Expr.t +Type error: Terms are not <= for cumulativity: Sort([Stdlib.Init.Datatypes.23,Stdlib.Init.Datatypes.24]) Sort([Set]) after reduction: Sort([Stdlib.Init.Datatypes.23,Stdlib.Init.Datatypes.24]) Sort([Set]), while checking MetaCoq.Template.Universes.Universe.Expr.t *) (* Unset Universe Minimization ToSet. *) -(* From Coq Require Import Decimal. *) -From Coq Require Import Decimal. +(* From Stdlib Require Import Decimal. *) +From Stdlib Require Import Decimal. Definition bignat : nat := Nat.of_num_uint 10000%uint. MetaCoq SafeCheck bignat. MetaCoq CoqCheck bignat. diff --git a/test-suite/unfold.v b/test-suite/unfold.v index 56513b90c..97474e5a3 100644 --- a/test-suite/unfold.v +++ b/test-suite/unfold.v @@ -3,4 +3,4 @@ From MetaCoq.Template Require Import All. Import MCMonadNotation. MetaCoq Test Quote negb. -MetaCoq Run (tmBind (tmEval (unfold (MPfile ["Datatypes"; "Init"; "Coq"], "negb")) negb) tmPrint). +MetaCoq Run (tmBind (tmEval (unfold (MPfile ["Datatypes"; "Init"; "Stdlib"], "negb")) negb) tmPrint). diff --git a/test-suite/univ.v b/test-suite/univ.v index 26ef6cb9e..d9de31ea6 100644 --- a/test-suite/univ.v +++ b/test-suite/univ.v @@ -120,30 +120,30 @@ MetaCoq Unquote Definition uqf := qf. Inductive foo (A : Type) : Type := | fooc : list A -> foo A. (* Print Universes.*) -(* Top.1 <= Coq.Init.Datatypes.44 *) +(* Top.1 <= Stdlib.Init.Datatypes.44 *) MetaCoq Quote Recursively Definition qfoo := foo. (* Compute qfoo. *) Polymorphic Inductive foo2 (A : Type) : Type := | fooc2 : list A -> foo2 A. -(* Top.4 |= Top.4 <= Coq.Init.Datatypes.44 *) +(* Top.4 |= Top.4 <= Stdlib.Init.Datatypes.44 *) (* Print Universes.*) Definition foo2_instance := foo2. (* Print Universes.*) -(* Top.9 <= Coq.Init.Datatypes.44 *) +(* Top.9 <= Stdlib.Init.Datatypes.44 *) MetaCoq Quote Recursively Definition qfoo2 := foo2. (* Compute qfoo2. *) -(* (Level.lvar 0, Le, Level.level "Coq.Init.Datatypes.44") *) +(* (Level.lvar 0, Le, Level.level "Stdlib.Init.Datatypes.44") *) Polymorphic Inductive foo3@{i j k l} (A : Type@{i}) (B : Type@{j}) : Type@{k} := | fooc3 : @eq Type@{l} (list A) B-> foo3 A B. -(* i j k l |= l < Coq.Init.Logic.8 +(* i j k l |= l < Stdlib.Init.Logic.8 Set <= l i <= l - i <= Coq.Init.Datatypes.44 + i <= Stdlib.Init.Datatypes.44 j <= l *) MetaCoq Quote Recursively Definition qfoo3 := foo3. (* Compute qfoo3. *) diff --git a/test-suite/vs.v b/test-suite/vs.v index 7073f8d5a..4ba7aabfa 100755 --- a/test-suite/vs.v +++ b/test-suite/vs.v @@ -3,12 +3,12 @@ Require Import BinPos. Require Import Lia. Require Import Recdef. -Require Import Coq.Lists.List. +Require Import Stdlib.Lists.List. Require Import ZArith. Require Import NArith. Require Import List Orders POrderedType. Require Import Sorted. -Require Import Coq.Sorting.Mergesort. +Require Import Stdlib.Sorting.Mergesort. Require Import Permutation. Set Implicit Arguments. @@ -406,8 +406,8 @@ Qed. (* clauses.v *) Unset Implicit Arguments. -Require Import ZArith List Recdef Coq.MSets.MSetInterface Coq.Sorting.Mergesort - Permutation Coq.MSets.MSetAVL Coq.MSets.MSetRBT. +Require Import ZArith List Recdef Stdlib.MSets.MSetInterface Stdlib.Sorting.Mergesort + Permutation Stdlib.MSets.MSetAVL Stdlib.MSets.MSetRBT. (** The clause datatype and related definitions and lemmas *) @@ -967,7 +967,7 @@ Require Import Finite_sets_facts. the axioms used by MSL and by the CompCert project. *) -Require Coq.Logic.ClassicalFacts. +Require Stdlib.Logic.ClassicalFacts. (** * Extensionality axioms *) @@ -983,7 +983,7 @@ Lemma functional_extensionality {A B} (f g : A -> B) : (forall x, f x = g x) -> f = g. >> *) -Require Export Coq.Logic.FunctionalExtensionality. +Require Export Stdlib.Logic.FunctionalExtensionality. (** For compatibility with earlier developments, [extensionality] is an alias for [functional_extensionality]. *) diff --git a/translations/MiniHoTT.v b/translations/MiniHoTT.v index 7b32f3f48..c3c8e6b45 100644 --- a/translations/MiniHoTT.v +++ b/translations/MiniHoTT.v @@ -64,7 +64,7 @@ Arguments symmetry {A R _} / _ _ _. Arguments transitivity {A R _} / {_ _ _} _ _. Ltac reflexivity := - Coq.Init.Ltac.reflexivity + Stdlib.Init.Ltac.reflexivity || (intros; let R := match goal with |- ?R ?x ?y => constr:(R) end in let pre_proof_term_head := constr:(@reflexivity _ R _) in diff --git a/translations/MiniHoTT_paths.v b/translations/MiniHoTT_paths.v index 5aceff785..514994817 100644 --- a/translations/MiniHoTT_paths.v +++ b/translations/MiniHoTT_paths.v @@ -67,7 +67,7 @@ Arguments symmetry {A R _} / _ _ _. Arguments transitivity {A R _} / {_ _ _} _ _. Ltac reflexivity := - Coq.Init.Ltac.reflexivity + Stdlib.Init.Ltac.reflexivity || (intros; let R := match goal with |- ?R ?x ?y => constr:(R) end in let pre_proof_term_head := constr:(@reflexivity _ R _) in diff --git a/translations/param_cheap_packed.v b/translations/param_cheap_packed.v index fc79ffc3f..0dfa251c9 100644 --- a/translations/param_cheap_packed.v +++ b/translations/param_cheap_packed.v @@ -418,7 +418,7 @@ Check (consᵗ : forall (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l), (* About tuᵗ. *) -(* Definition nat_entryT := Eval vm_compute in match tsl_mind_entry ([], []) "Coq.Init.Datatypes.nat" nat_entry with | Success (_, [e]) => e | _ => todo end. *) +(* Definition nat_entryT := Eval vm_compute in match tsl_mind_entry ([], []) "Stdlib.Init.Datatypes.nat" nat_entry with | Success (_, [e]) => e | _ => todo end. *) (* MetaCoq Unquote Inductive nat_entryT. *) (* Check (natᵗ : nat -> Set). *) (* Check (Oᵗ : natᵗ O). *) @@ -426,8 +426,8 @@ Check (consᵗ : forall (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l), (* MetaCoq Quote Recursively Definition bool_prog := bool. *) (* Definition bool_entry := Eval compute in *) -(* (mind_body_to_entry (option_get todo (extract_mind_body_from_program "Coq.Init.Datatypes.bool" bool_prog) )). *) -(* Definition bool_entryT := Eval vm_compute in match tsl_mind_entry ([], []) "Coq.Init.Datatypes.bool" bool_entry with | Success (_, [e]) => e | _ => todo end. *) +(* (mind_body_to_entry (option_get todo (extract_mind_body_from_program "Stdlib.Init.Datatypes.bool" bool_prog) )). *) +(* Definition bool_entryT := Eval vm_compute in match tsl_mind_entry ([], []) "Stdlib.Init.Datatypes.bool" bool_entry with | Success (_, [e]) => e | _ => todo end. *) (* MetaCoq Unquote Inductive bool_entryT. *) @@ -441,7 +441,7 @@ Check (consᵗ : forall (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l), (* (* (* MetaCoq Quote Definition tnatT := (nat; natᵗ). *) *) *) (* (* (* MetaCoq Quote Definition tOT := Oᵗ. *) *) *) (* (* (* MetaCoq Quote Definition tST := Sᵗ. *) *) *) -(* (* Definition vect_entryT := Eval vm_compute in match tsl_mind_entry ([InductiveDecl "Coq.Init.Datatypes.nat" nat_decl], [(IndRef (mkInd "Coq.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) 1, tST)]) "Top.t" vect_entry *) *) +(* (* Definition vect_entryT := Eval vm_compute in match tsl_mind_entry ([InductiveDecl "Stdlib.Init.Datatypes.nat" nat_decl], [(IndRef (mkInd "Stdlib.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) 1, tST)]) "Top.t" vect_entry *) *) (* (* with | Success (_, [e]) => e | _ => todo end. *) *) (* (* (* Definition vect_entryT' := . *) *) *) (* (* MetaCoq Unquote Inductive vect_entryT. *) *) @@ -449,17 +449,17 @@ Check (consᵗ : forall (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l), (* (* (* Require Vectors.VectorDef. *) *) *) (* (* (* MetaCoq Quote Recursively Definition vect_prog := Vectors.VectorDef.t. *) *) *) (* (* (* Definition vect_decl := Eval compute in *) *) *) -(* (* (* extract_mind_body_from_program "Coq.Vectors.VectorDef.t" vect_prog. *) *) *) +(* (* (* extract_mind_body_from_program "Stdlib.Vectors.VectorDef.t" vect_prog. *) *) *) (* (* (* Definition vect_entry := Eval compute in *) *) *) (* (* (* (mind_body_to_entry (option_get todo_coq vect_decl)). *) *) *) (* (* (* (* MetaCoq Unquote Inductive vect_entry. *) *) *) *) -(* (* (* Definition vect_entryT := Eval vm_compute in tsl_mind_entry [InductiveDecl "Coq.Init.Datatypes.nat" nat_decl] [(IndRef (mkInd "Coq.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) 1, tST)] "Coq.Vectors.VectorDef.t" vect_entry. *) *) *) +(* (* (* Definition vect_entryT := Eval vm_compute in tsl_mind_entry [InductiveDecl "Stdlib.Init.Datatypes.nat" nat_decl] [(IndRef (mkInd "Stdlib.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) 1, tST)] "Stdlib.Vectors.VectorDef.t" vect_entry. *) *) *) (* (* (* (* Definition vect_entryT' := . *) *) *) *) (* (* (* MetaCoq Unquote Inductive vect_entryT. *) *) *) (* (* Check tᵗ : forall (A : exists A : Set, A -> Set) (N : exists n, natᵗ n), t A.1 N.1 -> Set. *) *) -(* (* Definition eq_entryT := Eval vm_compute in tsl_mind_entry [] [] "Coq.Init.Datatypes.eq" eq_entry. *) *) +(* (* Definition eq_entryT := Eval vm_compute in tsl_mind_entry [] [] "Stdlib.Init.Datatypes.eq" eq_entry. *) *) (* (* Definition eq'_entry := Eval compute in *) *) (* (* (mind_body_to_entry (option_get todo_coq eq'_decl)). *) *) (* (* Definition eq'_entryT := Eval vm_compute in tsl_mind_entry [] [] "Top.eq'" eq'_entry. *) *) @@ -488,13 +488,13 @@ Check (consᵗ : forall (A : TYPE) (x : El A) (lH : ∃ l, listᵗ A l), (* (* Definition even_entry := Eval compute in *) *) (* (* (mind_body_to_entry *) *) (* (* (option_get todo_coq *) *) -(* (* (extract_mind_body_from_program "Coq.Arith.Even.even" even_prog) *) *) +(* (* (extract_mind_body_from_program "Stdlib.Arith.Even.even" even_prog) *) *) (* (* )). *) *) (* (* (* MetaCoq Unquote Inductive even_entry. *) *) *) (* (* (* Inductive even : nat -> Prop := *) *) *) (* (* (* even_O : even 0 | even_S : forall n : nat, odd n -> even (S n) *) *) *) (* (* (* with odd : nat -> Prop := odd_S : forall n : nat, even n -> odd (S n) *) *) *) -(* (* Definition even_entryT := Eval vm_compute in tsl_mind_entry [InductiveDecl "Coq.Init.Datatypes.nat" nat_decl] [(IndRef (mkInd "Coq.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Coq.Init.Datatypes.nat" 0) 1, tST)] "Coq.Arith.Even.even" even_entry. *) *) +(* (* Definition even_entryT := Eval vm_compute in tsl_mind_entry [InductiveDecl "Stdlib.Init.Datatypes.nat" nat_decl] [(IndRef (mkInd "Stdlib.Init.Datatypes.nat" 0), tnatT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) O, tOT); (ConstructRef (mkInd "Stdlib.Init.Datatypes.nat" 0) 1, tST)] "Stdlib.Arith.Even.even" even_entry. *) *) (* (* MetaCoq Unquote Inductive even_entryT. *) *) (* (* Check evenᵗ : forall (N : exists n, natᵗ n), even N.1 -> Prop. *) *) (* (* Check oddᵗ : forall (N : exists n, natᵗ n), odd N.1 -> Prop. *) *) diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v index d4824febd..1b699da01 100644 --- a/utils/theories/MCList.v +++ b/utils/theories/MCList.v @@ -1,5 +1,5 @@ From Equations Require Import Equations. -From Coq Require Import Bool Arith Lia SetoidList Utf8. +From Stdlib Require Import Bool Arith Lia SetoidList Utf8. From MetaCoq.Utils Require Import MCPrelude MCRelations. Set Equations Transparent. @@ -217,7 +217,7 @@ Section Reverse_Induction. forall P:list A-> Type, P [] -> (forall (a:A) (l:list A), P (List.rev l) -> P (List.rev (a :: l))) -> - forall l:list A, P (Coq.Lists.List.rev l). + forall l:list A, P (Stdlib.Lists.List.rev l). Proof using Type. induction l; auto. Qed. @@ -1519,4 +1519,4 @@ Qed. Lemma nth_error_firstn A n m (l:list A) x : nth_error (firstn n l) m = Some x -> nth_error l m = Some x. Proof. revert n l. induction m; intros n l H; destruct n, l; cbn in *; try solve [inversion H]; eauto. -Qed. \ No newline at end of file +Qed.