Merge paths

Author: proux01

.github/workflows/nix-action-coq-master.yml

@@ -6396,3 +6396,4 @@ name: Nix CI for bundle coq-master
   push:
     branches:
     - master
+    - squeezing-paths

.nix/config.nix

@@ -230,7 +230,7 @@ with builtins; with (import <nixpkgs> {}).lib;
     };
   in {
     "coq-master".coqPackages = common-bundles // {
-      coq.override.version = "proux01:stdlib_repo";
+      coq.override.version = "proux01:squeezing-paths";
     };
     "coq-master".ocamlPackages = {
       elpi.override.version = "1.19.2";

theories/Make.all

@@ -499,62 +499,62 @@ Wellfounded/Lexicographic_Exponentiation.v
 Wellfounded/List_Extension.v
 nsatz/NsatzTactic.v
 
--Q Arith/All Stdlib.Arith.All.Stdlib.Arith
--Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith
+-Q Arith/All Stdlib.Arith
+-Q 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 Classes/All Stdlib.Classes
+-Q Classes/Arith Stdlib.Classes
+-Q Classes/Lists Stdlib.Classes
 -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 Logic/Base Stdlib.Logic
+-Q Logic/Classical Stdlib.Logic
+-Q Logic/Lists Stdlib.Logic
 -Q MSets Stdlib.MSets
 -Q NArith Stdlib.NArith
 -Q Numbers/Cyclic Stdlib.Numbers.Cyclic
 -Q Numbers/Integer Stdlib.Numbers.Integer
 -Q Numbers/NatInt Stdlib.Numbers.NatInt
 -Q Numbers/Natural Stdlib.Numbers.Natural
--Q Numbers/Other Stdlib.Numbers.Other.Stdlib.Numbers
--Q Numbers/Q Stdlib.Numbers.Q.Stdlib.Numbers
--Q Numbers/R Stdlib.Numbers.R.Stdlib.Numbers
--Q Numbers/Strings Stdlib.Numbers.Strings.Stdlib.Numbers
--Q Numbers/Z Stdlib.Numbers.Z.Stdlib.Numbers
+-Q Numbers/Other Stdlib.Numbers.Other
+-Q Numbers/Q Stdlib.Numbers
+-Q Numbers/R Stdlib.Numbers
+-Q Numbers/Strings Stdlib.Numbers
+-Q Numbers/Z 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 Program/All Stdlib.Program
+-Q QArith/All Stdlib.QArith
+-Q QArith/Base Stdlib.QArith
+-Q QArith/Field Stdlib.QArith
 -Q Reals Stdlib.Reals
--Q Relations/All Stdlib.Relations.All.Stdlib.Relations
+-Q 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 Structures/Def Stdlib.Structures
+-Q 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 ZArith/All Stdlib.ZArith
+-Q ZArith/Base Stdlib.ZArith
+-Q 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 extraction/All Stdlib.extraction
+-Q 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 micromega/Int63 Stdlib.micromega
+-Q micromega/Lia Stdlib.micromega
+-Q micromega/Lqa Stdlib.micromega
+-Q micromega/Lra Stdlib.micromega
+-Q 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
+-Q setoid_ring/Q Stdlib.setoid_ring
+-Q setoid_ring/R Stdlib.setoid_ring
+-Q setoid_ring/Z Stdlib.setoid_ring