Add minor fixes for Coq 8.17 and 8.18

.github/workflows/coq-8.17.yml

@@ -0,0 +1,23 @@
+name: 8.16
+on: push
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - uses: coq-community/docker-coq-action@v1.4.1
+      with:
+        coq_version: "8.17"
+        ocaml_version: default
+        before_script: |
+          startGroup "Workaround permission issue"
+            sudo chown -R coq:coq .
+          endGroup
+        script: |
+          startGroup "Build project"
+            make
+          endGroup
+        after_script: |
+          startGroup "Revert permissions"
+            sudo chown -R 1001:116 .
+          endGroup

.github/workflows/coq-8.18.yml

@@ -0,0 +1,23 @@
+name: 8.16
+on: push
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - uses: coq-community/docker-coq-action@v1.4.1
+      with:
+        coq_version: "8.18"
+        ocaml_version: default
+        before_script: |
+          startGroup "Workaround permission issue"
+            sudo chown -R coq:coq .
+          endGroup
+        script: |
+          startGroup "Build project"
+            make
+          endGroup
+        after_script: |
+          startGroup "Revert permissions"
+            sudo chown -R 1001:116 .
+          endGroup

README.md

@@ -6,6 +6,8 @@ I'm currently running against time to finish everything, and I'm pretty tired,
 but I'll get back in here to improve this documentation.
 
 ![Coq 8.16](https://github.com/takanuva/cps/actions/workflows/coq-8.16.yml/badge.svg)
+![Coq 8.17](https://github.com/takanuva/cps/actions/workflows/coq-8.17.yml/badge.svg)
+![Coq 8.18](https://github.com/takanuva/cps/actions/workflows/coq-8.18.yml/badge.svg)
 
 # Summary of files
 

theories/Equational.v

@@ -628,7 +628,7 @@ Proof.
       assumption.
     + induction H; auto.
       inversion_clear H2.
-      simpl; f_equal; auto.
+      simpl; f_equal; auto;
       apply H; auto.
   - rewrite lift_distributes_over_bind.
     do 3 rewrite subst_distributes_over_bind.

theories/Lambda/Calculus.v

@@ -940,7 +940,7 @@ Proof.
       (* From H, of course! *)
       admit.
     + replace n with (i + j) by lia.
-      constructor; auto.
+      constructor; auto;
       now apply IHh.
   - dependent destruction H.
     rename n0 into k.
@@ -949,7 +949,7 @@ Proof.
       (* As above, from H0. *)
       admit.
     + replace n with (i + j) by lia.
-      constructor; auto.
+      constructor; auto;
       now apply IHh.
   - dependent destruction H.
     rename n0 into k.
@@ -958,7 +958,7 @@ Proof.
       (* Ditto. *)
       admit.
     + replace n with (i + j) by lia.
-      constructor; auto.
+      constructor; auto;
       now apply IHh.
   - dependent destruction H.
     rename n0 into k.
@@ -967,7 +967,7 @@ Proof.
       (* Ditto. *)
       admit.
     + replace n with (i + j) by lia.
-      constructor; auto.
+      constructor; auto;
       now apply IHh.
   - dependent destruction H.
     rename n0 into k.

theories/Metatheory.v

@@ -1677,7 +1677,7 @@ Proof.
     rewrite subst_distributes_over_jump.
     f_equal.
     + apply IHe.
-    + list induction over H.
+    + list induction over H;
       apply H.
   - rewrite lift_distributes_over_bind.
     rewrite subst_distributes_over_bind.