Merge branch '9.0-update' into 9.1-update

Author: jim-portegies

CHANGES.md

@@ -1,5 +1,15 @@
 # Change log for the coq-waterproof library
 
+## Version 3.1.0+9.1
+
+- 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.1-dev"
+version: "3.1.0+9.1"
 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.1-dev)
+ (version 3.1.0+9.1)
  (synopsis "Coq proofs in a style that resembles non-mechanized mathematical proofs")
  (depends rocq-core rocq-stdlib))

src/META.coq-waterproof

@@ -1,6 +1,6 @@
 package "plugin" (
     directory = "."
-    version = "3.0.1+9.0-dev"
+    version = "3.1.0+9.1"
     description = "Waterproof plugin"
     requires = "rocq-runtime.plugins.ltac rocq-runtime.plugins.ltac2"
     archive(byte) = "waterproof.cma"

src/g_waterproof.mlg

@@ -22,8 +22,8 @@ DECLARE PLUGIN "coq-waterproof.plugin"
 open Exceptions
 open Waterprove
 
-let waterproof_version : string = "3.0.1+9.1-dev"
-(*
+let waterproof_version : string = "3.1.0+9.1"
+
 (* 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 *)
 let add_scope s f =

tests/Notations/Reals.v

@@ -41,3 +41,6 @@ Abort.
 
 Goal & |0| + |3| ≤ |-3| + |0| ≤ 4 + |5|.
 Abort.
+
+Goal & |0| * | 3 | ≤ | 4 + 3 | - |5| ≤ 3 * |- 2 |.
+Abort.

theories/Notations/Reals.v

@@ -60,9 +60,9 @@ Definition cv_implies_cv_abs_to_l_abs := cv_cvabs.
   When using this in rewrites, $<$, $>$, etc. should bind stronger.
 *)
 
-Notation "| x |" := (Rabs x) (at level 40, format "| x |") : R_scope.
-Notation "|- x |" := (| (-x) |) (at level 40, x at next level, only parsing) : R_scope.
-Notation "｜ x - y ｜" := (R_dist x y) (at level 40, x at level 38, y at level 38, format "｜ x  -  y ｜") : R_scope.
+Notation "| x |" := (Rabs x) (at level 20, format "| x |") : R_scope.
+Notation "|- x |" := (| (-x) |) (at level 20, x at next level, only parsing) : R_scope.
+Notation "｜ x - y ｜" := (R_dist x y) (at level 20, x at level 38, y at level 38, format "｜ x  -  y ｜") : R_scope.
 
 (** ** Powers *)
 Notation "a ³" := (a * a * a) (at level 1) : R_scope.