Update CHANGES.md and version number

Author: jim-portegies

CHANGES.md

@@ -1,5 +1,15 @@
 # Change log for the coq-waterproof library
 
+## Version 3.1.0+9.0
+
+- No longer throw an error if there are unused lemmas (this speeds up automation when using `By ... it holds that ...`)
+- Remove parentheses in suggestions
+- Fix issue with keywords
+- Allow for multiple reasons in `By ...`-clause
+- Add framework for registering definitions and alternative characterizations
+- Add Expand All functionality to Help
+- Simplify ffi mechanism
+
 ## Version 3.0.0+9.0
 
 - Remove need for parentheses in many places

coq-waterproof.opam

@@ -1,11 +1,12 @@
 opam-version: "2.0"
 name: "coq-waterproof"
-version: "3.0.1+9.0-dev"
+version: "3.1.0+9.0"
 maintainer: "Jim Portegies <[email protected]>"
 authors: [
   "Jelle Wemmenhove"
   "Pim Otte"
   "Balthazar Pathiachvili"
+  "Dick Arends"
   "Cosmin Manea"
   "Lulof Pirée"
   "Adrian Vrămuleţ"

dune-project

@@ -5,6 +5,6 @@
 
 (package
  (name coq-waterproof)
- (version 3.0.1+9.0-dev)
+ (version 3.1.0+9.0)
  (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.1.0+9.0"
 
 (* 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 *)