diff --git a/theories/Make.all b/theories/Make.all index 34889c2dca..4c74e4b2e3 100644 --- a/theories/Make.all +++ b/theories/Make.all @@ -503,4 +503,55 @@ Wellfounded/Lexicographic_Product.v Wellfounded/Lexicographic_Exponentiation.v nsatz/NsatzTactic.v --Q . Stdlib +-Q Arith/All Stdlib.Arith.All.Stdlib.Arith +-Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith +-Q Array Stdlib.Array +-Q Bool Stdlib.Bool +-Q Classes/All Stdlib.Classes.All.Stdlib.Classes +-Q Classes/Arith Stdlib.Classes.Arith.Stdlib.Classes +-Q Classes/Lists Stdlib.Classes.Lists.Stdlib.Classes +-Q Compat Stdlib.Compat +-Q FSets Stdlib.FSets +-Q Floats Stdlib.Floats +-Q Lists Stdlib.Lists +-Q Logic/Base Stdlib.Logic.Base.Stdlib.Logic +-Q Logic/Classical Stdlib.Logic.Classical.Stdlib.Logic +-Q Logic/Lists Stdlib.Logic.Lists.Stdlib.Logic +-Q MSets Stdlib.MSets +-Q NArith Stdlib.NArith +-Q Numbers Stdlib.Numbers +-Q PArith Stdlib.PArith +-Q Program/All Stdlib.Program.All.Stdlib.Program +-Q QArith/All Stdlib.QArith.All.Stdlib.QArith +-Q QArith/Base Stdlib.QArith.Base.Stdlib.QArith +-Q QArith/Field Stdlib.QArith.Field.Stdlib.QArith +-Q Reals Stdlib.Reals +-Q Relations/All Stdlib.Relations.All.Stdlib.Relations +-Q Sets Stdlib.Sets +-Q Sorting Stdlib.Sorting +-Q Streams Stdlib.Streams +-Q Strings Stdlib.Strings +-Q Structures/Def Stdlib.Structures.Def.Stdlib.Structures +-Q Structures/Ex Stdlib.Structures.Ex.Stdlib.Structures +-Q Unicode Stdlib.Unicode +-Q Vectors Stdlib.Vectors +-Q Wellfounded Stdlib.Wellfounded +-Q ZArith/All Stdlib.ZArith.All.Stdlib.ZArith +-Q ZArith/Base Stdlib.ZArith.Base.Stdlib.ZArith +-Q ZArith/Ring Stdlib.ZArith.Ring.Stdlib.ZArith +-Q btauto Stdlib.btauto +-Q derive Stdlib.derive +-Q extraction/All Stdlib.extraction.All.Stdlib.extraction +-Q extraction/Base Stdlib.extraction.Base.Stdlib.extraction +-Q funind Stdlib.funind +-Q micromega/Int63 Stdlib.micromega.Int63.Stdlib.micromega +-Q micromega/Lia Stdlib.micromega.Lia.Stdlib.micromega +-Q micromega/Lqa Stdlib.micromega.Lqa.Stdlib.micromega +-Q micromega/Lra Stdlib.micromega.Lra.Stdlib.micromega +-Q micromega/Zify Stdlib.micromega.Zify.Stdlib.micromega +-Q nsatz Stdlib.nsatz +-Q omega Stdlib.omega +-Q rtauto Stdlib.rtauto +-Q setoid_ring/Q Stdlib.setoid_ring.Q.Stdlib.setoid_ring +-Q setoid_ring/R Stdlib.setoid_ring.R.Stdlib.setoid_ring +-Q setoid_ring/Z Stdlib.setoid_ring.Z.Stdlib.setoid_ring diff --git a/theories/Make.arith b/theories/Make.arith index 79c523544e..99c927ca91 100644 --- a/theories/Make.arith +++ b/theories/Make.arith @@ -1,3 +1,3 @@ Arith/All/Arith.v --Q Arith/All Stdlib.Arith.All +-Q Arith/All Stdlib.Arith.All.Stdlib.Arith diff --git a/theories/Make.arith-base b/theories/Make.arith-base index f9524442c6..d46ee9c00b 100644 --- a/theories/Make.arith-base +++ b/theories/Make.arith-base @@ -52,6 +52,6 @@ Numbers/Natural/Abstract/NLcm.v Numbers/Natural/Abstract/NOrder.v Classes/Arith/SetoidDec.v --Q Arith/Base Stdlib.Arith.Base +-Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith -Q Numbers Stdlib.Numbers --Q Classes/Arith Stdlib.Classes.Arith +-Q Classes/Arith Stdlib.Classes.Arith.Stdlib.Classes diff --git a/theories/Make.classes b/theories/Make.classes index 92af700b81..1a9782679d 100644 --- a/theories/Make.classes +++ b/theories/Make.classes @@ -4,4 +4,4 @@ Classes/All/Morphisms_Relations.v Classes/All/RelationPairs.v Classes/All/SetoidClass.v --Q Classes/All Stdlib.Classes.All +-Q Classes/All Stdlib.Classes.All.Stdlib.Classes diff --git a/theories/Make.classical-logic b/theories/Make.classical-logic index 0af170b74a..1594562a53 100644 --- a/theories/Make.classical-logic +++ b/theories/Make.classical-logic @@ -14,4 +14,4 @@ Logic/Classical/ClassicalUniqueChoice.v Logic/Classical/SetoidChoice.v Logic/Classical/Diaconescu.v --Q Logic/Classical Stdlib.Logic.Classical +-Q Logic/Classical Stdlib.Logic.Classical.Stdlib.Logic diff --git a/theories/Make.extraction b/theories/Make.extraction index 207c9c6fab..b349de5e84 100644 --- a/theories/Make.extraction +++ b/theories/Make.extraction @@ -20,4 +20,4 @@ extraction/All/ExtrOCamlInt63.v extraction/All/ExtrHaskellBasic.v extraction/All/ExtrHaskellNatInteger.v --Q extraction/All Stdlib.extraction.All +-Q extraction/All Stdlib.extraction.All.Stdlib.extraction diff --git a/theories/Make.extraction-base b/theories/Make.extraction-base index 59d7675f59..5f8f4956a9 100644 --- a/theories/Make.extraction-base +++ b/theories/Make.extraction-base @@ -1,3 +1,3 @@ extraction/Base/Extraction.v --Q extraction/Base Stdlib.extraction.Base +-Q extraction/Base Stdlib.extraction.Base.Stdlib.extraction diff --git a/theories/Make.field b/theories/Make.field index fe270a4256..2394f7b5a0 100644 --- a/theories/Make.field +++ b/theories/Make.field @@ -8,5 +8,5 @@ setoid_ring/Q/Field_tac.v setoid_ring/Q/Rings_Q.v setoid_ring/Q/Field.v --Q QArith/Field Stdlib.QArith.Field --Q setoid_ring/Q Stdlib.setoid_ring.Q +-Q QArith/Field Stdlib.QArith.Field.Stdlib.QArith +-Q setoid_ring/Q Stdlib.setoid_ring.Q.Stdlib.setoid_ring diff --git a/theories/Make.lia b/theories/Make.lia index 1b4d06d3d5..1efdfd1b20 100644 --- a/theories/Make.lia +++ b/theories/Make.lia @@ -23,5 +23,5 @@ micromega/Lia/ZCoeff.v micromega/Lia/RingMicromega.v -Q omega Stdlib.omega --Q micromega/Zify Stdlib.micromega.Zify --Q micromega/Lia Stdlib.micromega.Lia +-Q micromega/Zify Stdlib.micromega.Zify.Stdlib.micromega +-Q micromega/Lia Stdlib.micromega.Lia.Stdlib.micromega diff --git a/theories/Make.list b/theories/Make.list index c4a79d3d6c..3218b681fc 100644 --- a/theories/Make.list +++ b/theories/Make.list @@ -8,5 +8,5 @@ Classes/Lists/EquivDec.v -Q Lists Stdlib.Lists -Q Numbers Stdlib.Numbers --Q Logic/Lists Stdlib.Logic.Lists --Q Classes/Lists Stdlib.Classes.Lists +-Q Logic/Lists Stdlib.Logic.Lists.Stdlib.Logic +-Q Classes/Lists Stdlib.Classes.Lists.Stdlib.Classes diff --git a/theories/Make.logic b/theories/Make.logic index 27c6601434..cc267f06a2 100644 --- a/theories/Make.logic +++ b/theories/Make.logic @@ -20,4 +20,4 @@ Logic/Base/EqdepFacts.v Logic/Base/Hurkens.v Logic/Base/RelationalChoice.v --Q Logic/Base Stdlib.Logic.Base +-Q Logic/Base Stdlib.Logic.Base.Stdlib.Logic diff --git a/theories/Make.lqa b/theories/Make.lqa index ecda7a9abd..62990510c8 100644 --- a/theories/Make.lqa +++ b/theories/Make.lqa @@ -2,4 +2,4 @@ micromega/Lqa/QMicromega.v micromega/Lqa/Lqa.v micromega/Lqa/DeclConstant.v --Q micromega/Lqa Stdlib.micromega.Lqa +-Q micromega/Lqa Stdlib.micromega.Lqa.Stdlib.micromega diff --git a/theories/Make.orders-ex b/theories/Make.orders-ex index c121d6695f..20dc6441f8 100644 --- a/theories/Make.orders-ex +++ b/theories/Make.orders-ex @@ -9,4 +9,4 @@ Structures/Ex/OrderedTypeEx.v Structures/Ex/OrdersAlt.v Structures/Ex/DecidableTypeEx.v --Q Structures/Ex Stdlib.Structures.Ex +-Q Structures/Ex Stdlib.Structures.Ex.Stdlib.Structures diff --git a/theories/Make.primitive-int b/theories/Make.primitive-int index 6b645c3e5f..659835b610 100644 --- a/theories/Make.primitive-int +++ b/theories/Make.primitive-int @@ -9,4 +9,4 @@ micromega/Int63/ZifyUint63.v micromega/Int63/ZifySint63.v -Q Numbers/Cyclic Stdlib.Numbers.Cyclic --Q micromega/Int63 Stdlib.micromega.Int63 +-Q micromega/Int63 Stdlib.micromega.Int63.Stdlib.micromega diff --git a/theories/Make.program b/theories/Make.program index 4ba85d6deb..f88e297d55 100644 --- a/theories/Make.program +++ b/theories/Make.program @@ -5,4 +5,4 @@ Program/All/WfExtensionality.v Program/All/Program.v Program/All/Combinators.v --Q Program/All Stdlib.Program.All +-Q Program/All Stdlib.Program.All.Stdlib.Program diff --git a/theories/Make.qarith b/theories/Make.qarith index 4cc766110e..255b0f1ba6 100644 --- a/theories/Make.qarith +++ b/theories/Make.qarith @@ -4,5 +4,5 @@ QArith/All/QArith.v Numbers/Q/DecimalQ.v Numbers/Q/HexadecimalQ.v --Q QArith/All Stdlib.QArith.All +-Q QArith/All Stdlib.QArith.All.Stdlib.QArith -Q Numbers/Q Stdlib.Numbers.Number.Q diff --git a/theories/Make.qarith-base b/theories/Make.qarith-base index 088d8b801d..5574e86fe5 100644 --- a/theories/Make.qarith-base +++ b/theories/Make.qarith-base @@ -3,4 +3,4 @@ QArith/Base/Qminmax.v QArith/Base/QOrderedType.v QArith/Base/QArith_base.v --Q QArith/Base Stdlib.QArith.Base +-Q QArith/Base Stdlib.QArith.Base.Stdlib.QArith diff --git a/theories/Make.reals b/theories/Make.reals index fb09e00a4a..17a5468b0b 100644 --- a/theories/Make.reals +++ b/theories/Make.reals @@ -93,6 +93,6 @@ Numbers/R/DecimalR.v Numbers/R/HexadecimalR.v -Q Reals Stdlib.Reals --Q setoid_ring/R Stdlib.setoid_ring.R --Q micromega/Lra Stdlib.micromega.Lra +-Q setoid_ring/R Stdlib.setoid_ring.R.Stdlib.setoid_ring +-Q micromega/Lra Stdlib.micromega.Lra.Stdlib.micromega -Q Numbers/R Stdlib.Numbers.R diff --git a/theories/Make.relations b/theories/Make.relations index c04770bf4c..e178f14490 100644 --- a/theories/Make.relations +++ b/theories/Make.relations @@ -2,4 +2,4 @@ Relations/All/Relation_Operators.v Relations/All/Operators_Properties.v Relations/All/Relations.v --Q Relations/All Stdlib.Relations.All +-Q Relations/All Stdlib.Relations.All.Stdlib.Relations diff --git a/theories/Make.ring b/theories/Make.ring index cc63e36e83..0bcade423b 100644 --- a/theories/Make.ring +++ b/theories/Make.ring @@ -21,5 +21,5 @@ setoid_ring/Z/ArithRing.v setoid_ring/Z/NArithRing.v setoid_ring/Z/Ring_theory.v --Q ZArith/Ring Stdlib.ZArith.Ring --Q setoid_ring/Z Stdlib.setoid_ring.Z +-Q ZArith/Ring Stdlib.ZArith.Ring.Stdlib.ZArith +-Q setoid_ring/Z Stdlib.setoid_ring.Z.Stdlib.setoid_ring diff --git a/theories/Make.structures b/theories/Make.structures index fe0860d5ae..e40212df17 100644 --- a/theories/Make.structures +++ b/theories/Make.structures @@ -4,4 +4,4 @@ Structures/Def/Orders.v Structures/Def/OrdersFacts.v Structures/Def/OrdersTac.v --Q Structures/Def Stdlib.Structures.Def +-Q Structures/Def Stdlib.Structures.Def.Stdlib.Structures diff --git a/theories/Make.zarith b/theories/Make.zarith index 63e46a611e..078b347f67 100644 --- a/theories/Make.zarith +++ b/theories/Make.zarith @@ -22,7 +22,7 @@ btauto/Algebra.v btauto/Reflect.v btauto/Btauto.v --Q ZArith/All Stdlib.ZArith.All +-Q ZArith/All Stdlib.ZArith.All.Stdlib.ZArith -Q Numbers/Natural/Binary Stdlib.Numbers.Natural.Binary -Q Numbers/Integer/Binary Stdlib.Numbers.Integer.Binary -Q Numbers/Integer/NatPairs Stdlib.Numbers.Integer.NatPairs diff --git a/theories/Make.zarith-base b/theories/Make.zarith-base index 7c135c3357..30fb24275d 100644 --- a/theories/Make.zarith-base +++ b/theories/Make.zarith-base @@ -38,4 +38,4 @@ ZArith/Base/Zeuclid.v ZArith/Base/Int.v -Q Numbers/Integer/Abstract Stdlib.Numbers.Integer.Abstract --Q ZArith/Base Stdlib.ZArith.Base +-Q ZArith/Base Stdlib.ZArith.Base.Stdlib.ZArith diff --git a/theories/_CoqProject b/theories/_CoqProject index d07b354629..9930c4f12c 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -1 +1,52 @@ --Q . Stdlib +-Q Arith/All Stdlib.Arith.All.Stdlib.Arith +-Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith +-Q Array Stdlib.Array +-Q Bool Stdlib.Bool +-Q Classes/All Stdlib.Classes.All.Stdlib.Classes +-Q Classes/Arith Stdlib.Classes.Arith.Stdlib.Classes +-Q Classes/Lists Stdlib.Classes.Lists.Stdlib.Classes +-Q Compat Stdlib.Compat +-Q FSets Stdlib.FSets +-Q Floats Stdlib.Floats +-Q Lists Stdlib.Lists +-Q Logic/Base Stdlib.Logic.Base.Stdlib.Logic +-Q Logic/Classical Stdlib.Logic.Classical.Stdlib.Logic +-Q Logic/Lists Stdlib.Logic.Lists.Stdlib.Logic +-Q MSets Stdlib.MSets +-Q NArith Stdlib.NArith +-Q Numbers Stdlib.Numbers +-Q PArith Stdlib.PArith +-Q Program/All Stdlib.Program.All.Stdlib.Program +-Q QArith/All Stdlib.QArith.All.Stdlib.QArith +-Q QArith/Base Stdlib.QArith.Base.Stdlib.QArith +-Q QArith/Field Stdlib.QArith.Field.Stdlib.QArith +-Q Reals Stdlib.Reals +-Q Relations/All Stdlib.Relations.All.Stdlib.Relations +-Q Sets Stdlib.Sets +-Q Sorting Stdlib.Sorting +-Q Streams Stdlib.Streams +-Q Strings Stdlib.Strings +-Q Structures/Def Stdlib.Structures.Def.Stdlib.Structures +-Q Structures/Ex Stdlib.Structures.Ex.Stdlib.Structures +-Q Unicode Stdlib.Unicode +-Q Vectors Stdlib.Vectors +-Q Wellfounded Stdlib.Wellfounded +-Q ZArith/All Stdlib.ZArith.All.Stdlib.ZArith +-Q ZArith/Base Stdlib.ZArith.Base.Stdlib.ZArith +-Q ZArith/Ring Stdlib.ZArith.Ring.Stdlib.ZArith +-Q btauto Stdlib.btauto +-Q derive Stdlib.derive +-Q extraction/All Stdlib.extraction.All.Stdlib.extraction +-Q extraction/Base Stdlib.extraction.Base.Stdlib.extraction +-Q funind Stdlib.funind +-Q micromega/Int63 Stdlib.micromega.Int63.Stdlib.micromega +-Q micromega/Lia Stdlib.micromega.Lia.Stdlib.micromega +-Q micromega/Lqa Stdlib.micromega.Lqa.Stdlib.micromega +-Q micromega/Lra Stdlib.micromega.Lra.Stdlib.micromega +-Q micromega/Zify Stdlib.micromega.Zify.Stdlib.micromega +-Q nsatz Stdlib.nsatz +-Q omega Stdlib.omega +-Q rtauto Stdlib.rtauto +-Q setoid_ring/Q Stdlib.setoid_ring.Q.Stdlib.setoid_ring +-Q setoid_ring/R Stdlib.setoid_ring.R.Stdlib.setoid_ring +-Q setoid_ring/Z Stdlib.setoid_ring.Z.Stdlib.setoid_ring