From df42b4b0d1d8090e4831e048545d66d8c970ee61 Mon Sep 17 00:00:00 2001 From: Nfsaavedra Date: Fri, 18 Oct 2024 15:09:25 +0100 Subject: [PATCH 1/2] Add 8.20 to GHA --- .github/workflows/test.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 216a95c..cb125cb 100644 --- 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 From 68a34f91a7fcb5f49cf911866c2b1b1d44300568 Mon Sep 17 00:00:00 2001 From: Nfsaavedra Date: Fri, 18 Oct 2024 15:41:04 +0100 Subject: [PATCH 2/2] fix tests --- coqpyt/tests/proof_file/expected/imports.yml | 3 +++ coqpyt/tests/proof_file/expected/valid_file.yml | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/coqpyt/tests/proof_file/expected/imports.yml b/coqpyt/tests/proof_file/expected/imports.yml index 82032e0..8915d0c 100644 --- 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 index 6496c18..4e1b4aa 100644 --- 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