Adapt to Rocq 9.0

Author: proux01

.github/workflows/docker-action.yml

@@ -5,7 +5,7 @@ name: Docker CI
 on:
   push:
     branches:
-      - master
+      - v9.0
   pull_request:
     branches:
       - '**'
@@ -17,10 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:9.0'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-paramcoq.opam'

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=v9.0
+[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
@@ -26,7 +26,7 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [doi-shield]: https://zenodo.org/badge/DOI/10.4230/LIPIcs.CSL.2012.381.svg
 [doi-link]: https://doi.org/10.4230/LIPIcs.CSL.2012.381
 
-A Coq plugin providing commands for generating parametricity statements.
+A Rocq plugin providing commands for generating parametricity statements.
 Typical applications of such statements are in data refinement proofs.
 Note that the plugin is still in an experimental state - it is not very user
 friendly (lack of good error messages) and still contains bugs. But it
@@ -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 v9.0 branch supports version 9.0 of Rocq, see releases for compatibility with released versions of Rocq
 - Additional dependencies: none
 - Coq namespace: `Param`
 - Related publication(s):

coq-paramcoq.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "Pierre Roux <pierre.roux@onera.fr>"
-version: "dev"
+version: "9.0.dev"
 
 homepage: "https://github.com/coq-community/paramcoq"
 dev-repo: "git+https://github.com/coq-community/paramcoq.git"
@@ -12,7 +12,7 @@ license: "MIT"
 
 synopsis: "Plugin for generating parametricity statements to perform refinement proofs"
 description: """
-A Coq plugin providing commands for generating parametricity statements.
+A Rocq plugin providing commands for generating parametricity statements.
 Typical applications of such statements are in data refinement proofs.
 Note that the plugin is still in an experimental state - it is not very user
 friendly (lack of good error messages) and still contains bugs. But it
@@ -24,11 +24,11 @@ install: [
   [make "-C" "test-suite" "examples"] {with-test}
 ]
 depends: [
-  "coq" {= "dev" }
+  "coq" {>= "9.0" & < "9.1~" }
 ]
 
 tags: [
-  "category:Miscellaneous/Coq Extensions"
+  "category:Miscellaneous/Rocq Extensions"
   "keyword:paramcoq"
   "keyword:parametricity"
   "keyword:OCaml modules"

meta.yml

@@ -6,12 +6,12 @@ community: true
 action: true
 plugin: true
 doi: 10.4230/LIPIcs.CSL.2012.381
-branch: 'master'
+branch: 'v9.0'
 
 synopsis: Plugin for generating parametricity statements to perform refinement proofs
 
 description: |-
-  A Coq plugin providing commands for generating parametricity statements.
+  A Rocq plugin providing commands for generating parametricity statements.
   Typical applications of such statements are in data refinement proofs.
   Note that the plugin is still in an experimental state - it is not very user
   friendly (lack of good error messages) and still contains bugs. But it
@@ -43,12 +43,12 @@ license:
 
 supported_coq_versions:
   text: >-
-    The master branch tracks the development version of Coq, see
-    releases for compatibility with released versions of Coq
-  opam: '{= "dev" }'
+    The v9.0 branch supports version 9.0 of Rocq, see
+    releases for compatibility with released versions of Rocq
+  opam: '{>= "9.0" & < "9.1~" }'
 
 categories:
-- name: 'Miscellaneous/Coq Extensions'
+- name: 'Miscellaneous/Rocq Extensions'
 
 keywords:
 - name: paramcoq
@@ -59,10 +59,10 @@ namespace: Param
 
 opam-file-maintainer: 'Pierre Roux <pierre.roux@onera.fr>'
 
-opam-file-version: 'dev'
+opam-file-version: '9.0.dev'
 
 tested_coq_opam_versions:
-- version: 'dev'
+- version: '9.0'
 
 documentation: |-
   ## Usage and Commands