Fixed compilation on Coq 8.17 and 8.18

weakmemory · May 10, 2024 · 5439684 · 5439684
1 parent 1025881
commit 5439684
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 5 deletions.
diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml
@@ -102,12 +102,14 @@ name: Nix CI for bundle 8.17
 'on':
   pull_request:
     paths:
-    - .github/workflows/**
+    - .github/workflows/nix-action-8.17.yml
   pull_request_target:
+    paths-ignore:
+    - .github/workflows/nix-action-8.17.yml
     types:
     - opened
     - synchronize
     - reopened
   push:
     branches:
-    - master
+    - '**'
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
@@ -112,4 +112,4 @@ name: Nix CI for bundle 8.18
     - reopened
   push:
     branches:
-    - master
+    - '**'
diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
@@ -112,4 +112,4 @@ name: Nix CI for bundle 8.19
     - reopened
   push:
     branches:
-    - master
+    - '**'
diff --git a/.nix/config.nix b/.nix/config.nix
@@ -33,12 +33,15 @@
   default-bundle = "8.19";
 
   bundles."8.17" = {
+    push-branches = [ "**" ];
     coqPackages.coq.override.version = "8.17";
   };
   bundles."8.18" = {
+    push-branches = [ "**" ];
     coqPackages.coq.override.version = "8.18";
   };
   bundles."8.19" = {
+    push-branches = [ "**" ];
     coqPackages.coq.override.version = "8.19";
   };
 

diff --git a/HahnCountable.v b/HahnCountable.v
@@ -22,7 +22,10 @@ Lemma findP_spec A (cond : A -> Prop) (l : list A)
   forall j, j < findP cond l -> ~ cond (nth j l d).
 Proof.
   induction l; ins; desf; splits; ins; desf; try lia; intuition.
-  eauto using PeanoNat.lt_S_n.
+  match goal with
+  | H' : S ?n < S _, H : forall x, _ |- _ => apply (H n); auto
+  end.
+  lia.
 Qed.
 
 Lemma exists_min (cond : nat -> Prop) (H: exists n, cond n) :
-Original file line number
+Diff line change
@@ Expand Up / @@ -112,4 +112,4 @@ name: Nix CI for bundle 8.18 @@
         - reopened
       push:
         branches:
-        - master
+        - '**'