Support also Coq 8.17 (besides Coq 8.18)

h0nzZik · Jan 22, 2024 · 1fba3e5 · 1fba3e5
1 parent 7c11a29
commit 1fba3e5
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/.github/workflows/build-and-profile.yml b/.github/workflows/build-and-profile.yml
@@ -34,7 +34,7 @@ jobs:
 
     - name: Build
       run: nix develop '.#minuska' --command ./build-and-profile.sh
-      
+
     - name: CoqDoc
       run: nix develop '.#minuska' --command make -C minuska/ html
 
@@ -45,6 +45,9 @@ jobs:
       with:
         path: 'minuska/html'
 
+    - name: 'Build with Coq 8.17'
+      run: nix build -L '.#minuska-coq_8_17'
+
   # Deployment job
   deploy:
     environment:

diff --git a/minuska/theories/benchmarking_in_coq.v b/minuska/theories/benchmarking_in_coq.v
@@ -86,7 +86,6 @@ Time Compute ("bench: imp-count-to(5)", (imp.interp_program_count_to 1000 5)).
 Time Compute ("bench: imp-count-to(6)", (imp.interp_program_count_to 1000 6)).
 Time Compute ("bench: imp-count-to(7)", (imp.interp_program_count_to 1000 7)).
 
-
 Time Compute (("bench: unary-fact(1)"),((unary_nat.interp_fact 5000 1).1)).
 Time Compute (("bench: unary-fact(2)"),((unary_nat.interp_fact 5000 2).1)).
 Time Compute (("bench: unary-fact(3)"),((unary_nat.interp_fact 5000 3).1)).

diff --git a/minuska/theories/try_match.v b/minuska/theories/try_match.v
@@ -1374,7 +1374,7 @@ Next Obligation.
                 inversion Hy.
             }
             {
-                symmetry. assumption.
+                ltac1:(congruence).
             }
         }
     }
@@ -1482,7 +1482,7 @@ Next Obligation.
             rewrite lookup_insert_ne in Hy.
             rewrite lookup_empty in Hy.
             { inversion Hy. }
-            { symmetry. assumption. }
+            { ltac1:(congruence). }
         }
     }
 Qed.