Rocq v9.0

.github/workflows/docker-action.yml

@@ -5,7 +5,7 @@ name: Docker CI
 on:
   push:
     branches:
-      - coq-master
+      - coq-v9.0
   pull_request:
     branches:
       - '**'
@@ -16,18 +16,16 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        coq_version:
-          - 'dev'
+        image:
+          - 'rocq/rocq-prover:9.0'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-dpdgraph.opam'
-          coq_version: ${{ matrix.coq_version }}
-          export: 'OPAMWITHTEST'
-        env:
-          OPAMWITHTEST: 'true'
+          custom_image: ${{ matrix.image }}
+
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/coq-dpdgraph/workflows/Docker%20CI/badge.svg?branch=coq-master
-[docker-action-link]: https://github.com/coq-community/coq-dpdgraph/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/coq-dpdgraph/actions/workflows/docker-action.yml/badge.svg?branch=coq-v9.0
+[docker-action-link]: https://github.com/coq-community/coq-dpdgraph/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
@@ -37,7 +37,7 @@ to visualize dependency graphs and find unused definitions.
   - Anne Pacalet ([**@Karmaki**](https://github.com/Karmaki))
   - Yves Bertot ([**@ybertot**](https://github.com/ybertot))
 - License: [GNU Lesser General Public License v2.1](LICENSE)
-- Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
+- Compatible Coq versions: 9.0 (use the corresponding branch or release for other Coq versions)
 - Compatible OCaml versions: 4.05.0 or later
 - Additional dependencies:
   - autoconf (except for releases)
@@ -102,16 +102,16 @@ instead of `make` in all previous commands.
 
 ### Install using opam
 
-If you use opam with the latest version of Coq, you can install 
-`coq-dpdgraph` and `ocamlgraph` using
+If you use opam with the latests version of Rocq you can install
+`coq-dpdgraph` and `ocamlgraph`using
 
     $ opam repo add coq-released https://coq.inria.fr/opam/released
     $ opam install coq-dpdgraph
 
-To install a specific release of `coq-dpdgraph` for a previous version of 
-Coq, add the appropriate suffix, for example,
+To install a specific release of `coq-dpdgraph`for a previous version of
+Rocq or Coq, add the appropriate suffix, for example,
 
-    $ opam install coq-dpdgraph.1.0+8.16
+    $ opam install coq-dpdgraph.1.0.8.16
 
 ### Test
 
@@ -264,7 +264,7 @@ Permutation_app_swap	(0)
 ```
 
 In the example above it reports that ``Permutation_app_swap`` was
-references 0 times.  You can specify max number of references allowed
+referenced 0 times.  You can specify max number of references allowed
 (default 0) via ``-threshold`` command line option.
 
 ## Development information

configure.ac

@@ -10,7 +10,7 @@
 # will set several variables: (see AC_SUBST at the end of this file)
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-AC_INIT(coq-dpdgraph,1.0)
+AC_INIT(coq-dpdgraph,1.0-9.0)
 AC_MSG_NOTICE(AC_PACKAGE_NAME version AC_PACKAGE_VERSION)
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

coq-dpdgraph.opam

@@ -22,7 +22,7 @@ run-test: [make "test-suite"]
 install: [make "install" "BINDIR=%{bin}%"]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "coq" {= "dev"}
+  "coq" {>= "9.0" & < "9.1~"}
   "conf-autoconf" {build & dev}
   "ocamlgraph" 
 ]

meta.yml

@@ -6,7 +6,7 @@ organization: coq-community
 community: true
 action: true
 plugin: true
-branch: 'coq-master'
+branch: 'coq-v9.0'
 
 synopsis: >-
   Compute dependencies between Coq objects (definitions, theorems) and produce graphs
@@ -29,15 +29,15 @@ maintainers:
 
 opam-file-maintainer: [email protected]
 
-opam-file-version: dev
+opam-file-version: 9.0
 
 license:
   fullname: GNU Lesser General Public License v2.1
   identifier: LGPL-2.1-only
 
 supported_coq_versions:
-  text: master (use the corresponding branch or release for other Coq versions)
-  opam: '{= "dev"}'
+  text: 9.0 (use the corresponding branch or release for other Coq versions)
+  opam: '{>= "9.0" & < "9.1~"}'
 
 supported_ocaml_versions:
     text: 4.05.0 or later
@@ -54,8 +54,8 @@ dependencies:
   description: |-
     [OCamlgraph](https://github.com/backtracking/ocamlgraph)
 
-tested_coq_opam_versions:
-- version: dev
+tested_rocq_opam_versions:
+- version: 9.0
 
 namespace: dpdgraph
 
@@ -124,11 +124,17 @@ build: |-
 
   ### Install using opam
 
-  If you use opam, you can install `coq-dpdgraph` and `ocamlgraph` using
+  If you use opam with the latests version of Rocq you can install
+  `coq-dpdgraph` and `ocamlgraph`using
 
       $ opam repo add coq-released https://coq.inria.fr/opam/released
       $ opam install coq-dpdgraph
 
+  To install a specific release of `coq-dpdgraph`for a previous version of
+  Rocq or Coq, add the appropriate suffix, for example,
+
+      $ opam install coq-dpdgraph.1.0.8.16
+
   ### Test
 
   If you install the archive by cloning the git repository, you have
@@ -281,7 +287,7 @@ documentation: |
   ```
 
   In the example above it reports that ``Permutation_app_swap`` was
-  references 0 times.  You can specify max number of references allowed
+  referenced 0 times.  You can specify max number of references allowed
   (default 0) via ``-threshold`` command line option.
 
   ## Development information

tests/PrimitiveProjections.v

@@ -3,6 +3,8 @@ Set Implicit Arguments.
 
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 
+Local Set Warnings "-notation-overridden".
+
 Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
 
 Definition bar := @projT1.

tests/Test.v

@@ -8,7 +8,7 @@
 
 (*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
 
-Require Import Arith Bool.
+From Stdlib Require Import Arith Bool.
 
 Set Implicit Arguments.