Add support for Coq 8.20 (#53)

sr-lab · Oct 18, 2024 · 17a16bc · 17a16bc
1 parent b718d1c
commit 17a16bc
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -17,6 +17,7 @@ jobs:
           - "8.17.1"
           - "8.18.0"
           - "8.19.2"
+          - "8.20.0"
 
     steps:
     - name: Checkout

diff --git a/coqpyt/tests/proof_file/expected/imports.yml b/coqpyt/tests/proof_file/expected/imports.yml
@@ -170,6 +170,9 @@ proofs:
       - "8.19.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "8.20.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION

diff --git a/coqpyt/tests/proof_file/expected/valid_file.yml b/coqpyt/tests/proof_file/expected/valid_file.yml
@@ -201,6 +201,9 @@ proofs:
       - "8.19.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "8.20.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
@@ -367,6 +370,9 @@ proofs:
       - "8.19.x":
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION
+        "8.20.x":
+          text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 10, x binder, y binder, P at level 200, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
+          type: NOTATION
         default:
           text: "Notation \"∀ x .. y , P\" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, format \"'[ ' '[ ' ∀ x .. y ']' , '/' P ']'\") : type_scope."
           type: NOTATION