From f703183b11d327aa0cdbae20e516f89c71e5303f Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 20 Jun 2024 09:51:49 +0200
Subject: [PATCH] Adapt to Coq 8.20

---
 .github/workflows/docker-action.yml |  4 ++--
 README.md                           |  6 +++---
 coq-paramcoq.opam                   |  4 ++--
 meta.yml                            | 10 +++++-----
 4 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 1dd5b98..8cd4f15 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -5,7 +5,7 @@ name: Docker CI
 on:
   push:
     branches:
-      - master
+      - v8.20
   pull_request:
     branches:
       - '**'
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index a692158..e66b39f 100644
--- a/README.md
+++ b/README.md
@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/paramcoq/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/paramcoq/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/paramcoq/actions/workflows/docker-action.yml/badge.svg?branch=v8.20
+[docker-action-link]: https://github.com/coq-community/paramcoq/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -45,7 +45,7 @@ is usable enough to "translate" a large chunk of the standard library.
 - Coq-community maintainer(s):
   - Pierre Roux ([**@proux01**](https://github.com/proux01))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: The master branch tracks the development version of Coq, see releases for compatibility with released versions of Coq
+- Compatible Coq versions: The v8.20 branch supports version 8.20 of Coq, see releases for compatibility with released versions of Coq
 - Additional dependencies: none
 - Coq namespace: `Param`
 - Related publication(s):
diff --git a/coq-paramcoq.opam b/coq-paramcoq.opam
index 1597b09..ee72737 100644
--- a/coq-paramcoq.opam
+++ b/coq-paramcoq.opam
@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "Pierre Roux <pierre.roux@onera.fr>"
-version: "dev"
+version: "8.20.dev"
 
 homepage: "https://github.com/coq-community/paramcoq"
 dev-repo: "git+https://github.com/coq-community/paramcoq.git"
@@ -24,7 +24,7 @@ install: [
   [make "-C" "test-suite" "examples"] {with-test}
 ]
 depends: [
-  "coq" {= "dev" }
+  "coq" {>= "8.20" & < "8.21~" }
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index d076736..ffb07f7 100644
--- a/meta.yml
+++ b/meta.yml
@@ -6,7 +6,7 @@ community: true
 action: true
 plugin: true
 doi: 10.4230/LIPIcs.CSL.2012.381
-branch: 'master'
+branch: 'v8.20'
 
 synopsis: Plugin for generating parametricity statements to perform refinement proofs
 
@@ -43,9 +43,9 @@ license:
 
 supported_coq_versions:
   text: >-
-    The master branch tracks the development version of Coq, see
+    The v8.20 branch supports version 8.20 of Coq, see
     releases for compatibility with released versions of Coq
-  opam: '{= "dev" }'
+  opam: '{>= "8.20" & < "8.21~" }'
 
 categories:
 - name: 'Miscellaneous/Coq Extensions'
@@ -59,10 +59,10 @@ namespace: Param
 
 opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'
 
-opam-file-version: 'dev'
+opam-file-version: '8.20.dev'
 
 tested_coq_opam_versions:
-- version: 'dev'
+- version: '8.20'
 
 documentation: |-
   ## Usage and Commands