update templates and generate boilerplate for 8.16

.github/workflows/docker-action.yml

@@ -5,7 +5,7 @@ name: Docker CI
 on:
   push:
     branches:
-      - master
+      - v8.16
   pull_request:
     branches:
       - '**'
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

.github/workflows/nix-action.yml

@@ -5,7 +5,7 @@ name: Nix CI
 on:
   push:
     branches:
-      - master
+      - v8.16
   pull_request:
     paths:
     - .github/workflows/**
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         overrides:
-          - 'coq = "master"'
+          - 'coq = "8.16"'
       fail-fast: false
     steps:
       - name: Determine which commit to test

README.md

@@ -12,10 +12,10 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/aac-tactics/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-shield]: https://github.com/coq-community/aac-tactics/workflows/Docker%20CI/badge.svg?branch=v8.16
 [docker-action-link]: https://github.com/coq-community/aac-tactics/actions?query=workflow:"Docker%20CI"
 
-[nix-action-shield]: https://github.com/coq-community/aac-tactics/workflows/Nix%20CI/badge.svg?branch=master
+[nix-action-shield]: https://github.com/coq-community/aac-tactics/workflows/Nix%20CI/badge.svg?branch=v8.16
 [nix-action-link]: https://github.com/coq-community/aac-tactics/actions?query=workflow:"Nix%20CI"
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
@@ -49,8 +49,8 @@ such as for binary integer arithmetic and booleans, are provided with the plugin
 - Coq-community maintainer(s):
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU Lesser General Public License v3.0 or later](LICENSE)
-- Compatible Coq versions: master (use the corresponding branch or release for other Coq versions)
-- Compatible OCaml versions: 4.05.0 or later
+- Compatible Coq versions: 8.16 (use the corresponding branch or release for other Coq versions)
+- Compatible OCaml versions: 4.09.0 or later
 - Additional dependencies: none
 - Coq namespace: `AAC_tactics`
 - Related publication(s):

coq-aac-tactics.opam

@@ -8,6 +8,7 @@ version: "dev"
 homepage: "https://github.com/coq-community/aac-tactics"
 dev-repo: "git+https://github.com/coq-community/aac-tactics.git"
 bug-reports: "https://github.com/coq-community/aac-tactics/issues"
+doc: "https://coq-community.github.io/aac-tactics/"
 license: "LGPL-3.0-or-later"
 
 synopsis: "Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators"
@@ -21,9 +22,9 @@ such as for binary integer arithmetic and booleans, are provided with the plugin
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "ocaml" {>= "4.05.0"}
+  "ocaml" {>= "4.09.0"}
   "dune" {>= "2.5"}
-  "coq" {= "dev"}
+  "coq" {>= "8.16" & < "8.17~"}
 ]
 
 tags: [

meta.yml

@@ -7,7 +7,7 @@ action: true
 nix: true
 plugin: true
 doi: 10.1007/978-3-642-25379-9_14
-branch: master
+branch: 'v8.16'
 coqdoc: true
 coqdoc_index: docs/coqdoc/toc.html
 
@@ -49,18 +49,18 @@ license:
   identifier: LGPL-3.0-or-later
 
 supported_coq_versions:
-  text: master (use the corresponding branch or release for other Coq versions)
-  opam: '{= "dev"}'
+  text: 8.16 (use the corresponding branch or release for other Coq versions)
+  opam: '{>= "8.16" & < "8.17~"}'
 
 supported_ocaml_versions:
-    text: 4.05.0 or later
-    opam: '{>= "4.05.0"}'
+    text: 4.09.0 or later
+    opam: '{>= "4.09.0"}'
 
 tested_coq_nix_versions:
-- coq_version: 'master'
+- coq_version: '8.16'
 
 tested_coq_opam_versions:
-- version: dev
+- version: '8.16'
 
 namespace: AAC_tactics