Towards nominals

.github/workflows/nix-action-8.18.yml

@@ -186,9 +186,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
         job "equations"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      name: 'Building/fetching previous CI target: mathcomp-boot'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
-        job "mathcomp-ssreflect"
+        job "mathcomp-boot"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr

.github/workflows/nix-action-8.19.yml

@@ -186,9 +186,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
         job "equations"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      name: 'Building/fetching previous CI target: mathcomp-boot'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
-        job "mathcomp-ssreflect"
+        job "mathcomp-boot"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr

.github/workflows/nix-action-8.20.yml

@@ -186,9 +186,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
         job "equations"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      name: 'Building/fetching previous CI target: mathcomp-boot'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
-        job "mathcomp-ssreflect"
+        job "mathcomp-boot"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr

.github/workflows/nix-action-9.0.yml

@@ -186,9 +186,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
         job "equations"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      name: 'Building/fetching previous CI target: mathcomp-boot'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
-        job "mathcomp-ssreflect"
+        job "mathcomp-boot"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr

.github/workflows/nix-action-MC-dev.yml

@@ -111,9 +111,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "MC-dev"
         --argstr job "equations"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
+      name: 'Building/fetching previous CI target: mathcomp-boot'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "MC-dev"
-        --argstr job "mathcomp-ssreflect"
+        --argstr job "mathcomp-boot"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "MC-dev"

.gitignore

@@ -32,6 +32,7 @@ Makefile.coq.conf
 
 # markdown preview
 *.html
+*.css
 
 # Latex
 *.aux
@@ -58,3 +59,5 @@ Makefile.coq.conf
 
 # coqdoc
 docs/
+# Dune
+_build/

.nix/config.nix

@@ -86,6 +86,8 @@
     extructures.override.version = "master";
     deriving.job = false;
     deriving.override.version = "master";
+    mathcomp-bigenough.job = false;
+    mathcomp-bigenough.override.version = "master";
   };
 
   bundles."8.18".push-branches = ["main"];

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"2763e9535d104d31e70695165ed1679611dbe8f5"
+"d0b8d01909a77316106775de3716ddf328e221d7"

.nix/coq-overlays/ssprove/default.nix

@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, version ? null
 , equations
-, mathcomp-ssreflect
+, mathcomp-boot
 , mathcomp-analysis
 , mathcomp-experimental-reals
 , mathcomp-word
@@ -36,7 +36,7 @@
   release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
 
   propagatedBuildInputs = [equations
-                           mathcomp-ssreflect
+                           mathcomp-boot
                            mathcomp-analysis
                            mathcomp-experimental-reals
                            mathcomp-word

.nix/nixpkgs.nix

@@ -1,4 +1,4 @@
 fetchTarball {
-    url = "https://github.com/NixOS/nixpkgs/archive/d3f5b059bb95493886de9ef215f8e4c95fbe8c0d.tar.gz";
-    sha256 = "10h5aki8nq59lj59kc50dnhfqiv8b1mvbxvyvsi48fvznw4p32y0";
+    url = "https://github.com/NixOS/nixpkgs/archive/d026ceca14fe50451c9bc43af676d922f8826b7d.tar.gz";
+    sha256 = "02g1ymc11z86hv99plp93k88byybjaqsc2hazb1yis53lwzb9hr6";
   }