Update versions

Author: jim-portegies

.devcontainer/Dockerfile

@@ -1,5 +1,5 @@
-FROM rocq/rocq-prover:9.0-ocaml-4.14-flambda
+FROM rocq/rocq-prover:9.1-ocaml-4.14-flambda
 
 RUN opam update; \
-    opam install coq-lsp.0.2.3+9.0 -y; \
+    opam install coq-lsp.0.2.3+9.1 -y; \
     opam install ocaml-lsp-server -y

.github/workflows/build.yml

@@ -19,7 +19,7 @@ jobs:
       - name: Build plugin
         uses: coq-community/docker-coq-action@v1
         with:
-          custom_image: 'rocq/rocq-prover:9.0-ocaml-4.14-flambda'
+          custom_image: 'rocq/rocq-prover:9.1-ocaml-4.14-flambda'
           opam_file: 'coq-waterproof.opam'
           before_script: |
             startGroup "Install dependencies"

.github/workflows/doc.yml

@@ -32,7 +32,7 @@ jobs:
         uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-waterproof.opam'
-          custom_image: 'rocq/rocq-prover:9.0-ocaml-4.14-flambda'
+          custom_image: 'rocq/rocq-prover:9.1-ocaml-4.14-flambda'
           before_script: |
             startGroup "Install dependencies"
               sudo apt-get -y -q install binutils make csh g++ sed gawk autoconf automake autotools-dev

Developer-instructions.md

@@ -31,11 +31,11 @@ Most development is done based off the main branch, and then the following setup
 ```
 opam init
 eval $(opam env)
-opam install coq-lsp.0.2.3+9.0
+opam install coq-lsp.0.2.3+9.1
 opam install ocaml-lsp-server
 ```
-replacing 9.0 with the desired version of Rocq, or more generally, replacing
-0.2.3+9.0 by the desired version of coq-lsp.
+replacing 9.1 with the desired version of Rocq, or more generally, replacing
+0.2.3+9.1 by the desired version of coq-lsp.
 
 ### Creating the desired opam environment: advanced version for supporting multiple versions of Rocq
 

coq-waterproof.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "coq-waterproof"
-version: "3.0.1+9.0-dev"
+version: "3.0.1+9.1-dev"
 maintainer: "Jim Portegies <[email protected]>"
 authors: [
   "Jelle Wemmenhove"
@@ -25,8 +25,9 @@ bug-reports: "https://github.com/impermeable/coq-waterproof/issues"
 
 depends: [
   "ocaml" {>= "4.09.0"}
-  "rocq-prover" {>= "9.0" & < "9.1" | = "dev"}
-  "coq" {>= "9.0" & < "9.1" | = "dev"}
+  "rocq-core" {>= "9.1" & < "9.2"}
+  "rocq-stdlib" {>= "9"}
+  "coq" {>= "9.1" & < "9.2"}
   "dune" {>= "3.8"}
 ]
 

dune-project

@@ -5,6 +5,6 @@
 
 (package
  (name coq-waterproof)
- (version 3.0.1+9.0-dev)
+ (version 3.0.1+9.1-dev)
  (synopsis "Coq proofs in a style that resembles non-mechanized mathematical proofs")
  (depends rocq-core rocq-stdlib))

src/g_waterproof.mlg

@@ -22,7 +22,7 @@ DECLARE PLUGIN "coq-waterproof.plugin"
 open Exceptions
 open Waterprove
 
-let waterproof_version : string = "3.0.1+9.0-dev"
+let waterproof_version : string = "3.0.1+9.1-dev"
 (*
 (* The code below is a hack to patch in (open_)lconstr into Ltac2 *)
 (* It should be removed when merged to coq-master (open_)lconstr should be in release 9.1 *)