Test without overlays

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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