Refactor: incorporate some changes from 8.17 and update version numbers

CHANGES.md

@@ -1,5 +1,10 @@
 # Change log for the coq-waterproof library
 
+## Version 2.1.1+8.19
+
+- Compatibility with earlier OCaml compilers
+- Fixes for the strong induction tactic
+
 ## Version 2.1.0+8.17
 
 - Improve the `Either` tactic: now proves and destructs ordinary 'ors' when the goal is a proposition

coq-waterproof.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "coq-waterproof"
-version: "2.1.0+8.19"
+version: "2.1.1+8.19"
 maintainer: "Jim Portegies <j.w.portegies@tue.nl>"
 authors: [
   "Jelle Wemmenhove"

dune-project

@@ -3,6 +3,6 @@
 
 (package
  (name coq-waterproof)
- (version 2.1.0+8.19)
+ (version 2.1.1+8.19)
  (synopsis "Coq proofs in a style that resembles non-mechanized mathematical proofs")
  (depends coq-core coq-stdlib))

src/META.coq-waterproof

@@ -1,6 +1,6 @@
 package "waterproof" (
     directory = "."
-    version = "2.1.0+8.19"
+    version = "2.1.1+8.19"
     description = "Waterproof plugin"
     requires = "coq-core.plugins.ltac coq-core.plugins.ltac2"
     archive(byte) = "waterproof.cma"

src/g_waterproof.mlg

@@ -34,7 +34,7 @@ open Exceptions
 open Hint_dataset_declarations
 open Waterprove
 
-let waterproof_version : string = "2.1.0+8.19"
+let waterproof_version : string = "2.1.1+8.19"
 }
 
 VERNAC COMMAND EXTEND AutomationShieldEnableSideEff CLASSIFIED AS SIDEFF

theories/Libs/Analysis/Sequences.v

@@ -89,9 +89,12 @@ Proof.
     Either (x <= 0) or (0 < x).
     - Case (x <= 0).
       Choose n := 1%nat.
-      It holds that (INR n > INR 0).
-      It holds that (x <= 0%nat).
-      We conclude that (INR n > x).
+      We claim that (INR 1 > INR 0).
+      { We need to show that ( 1 > 0 ).
+        We conclude that (1 > 0).
+      }
+      It holds that (x <= INR 0).
+      We conclude that (n > x).
     - Case (0 < x).
       By archimed it holds that (IZR( up x) > x ∧ IZR( up x ) - x ≤ 1).
       It holds that (IZR( up x ) > x).

theories/Libs/Analysis/Subsequences.v

@@ -282,7 +282,7 @@ Proof.
           | 0 => f(0)
           | S k => Nat.max(f(l), seq_of_max(f, k))
           end)(g, n + 1))%nat.
-      It holds that (n + 1 = S n)%nat (i).
+      It holds that (n + 1 = S n)%nat.
       It suffices to show that (g(n) ≤ seq_of_max(g, n))%nat.
       We conclude that (g(n) ≤ seq_of_max(g, n))%nat.
 Qed.

theories/Util/Since.v

@@ -30,19 +30,13 @@ Local Ltac2 get_type (x: constr) : constr := eval unfold type_of in (type_of $x)
 
 Local Ltac2 check_if_not_reference (x : constr) :=
   let type_x := get_type x in
-  match check_constr_equal type_x constr:(Prop) with
-  | true => ()
-  | false => 
-    match check_constr_equal type_x constr:(Set) with
-    | true => ()
-    | false => 
-      match check_constr_equal type_x constr:(Type) with
-      | true => ()
-      | false => throw (concat_list
+  match! type_x with
+  | Prop => ()
+  | Set => ()
+  | Type => ()
+  | _ => throw (concat_list
         [of_string "Cannot use reference "; of_constr x; of_string " with `Since`.
 Try `By "; of_constr x; of_string " ...` instead."])
-      end
-    end
   end.
 
 Local Ltac2 check_if_not_statement (x : constr) :=
@@ -51,17 +45,11 @@ Local Ltac2 check_if_not_statement (x : constr) :=
 Try `Since "; of_constr x; of_string " ...` instead."]
   in
   let type_x := get_type x in
-  match check_constr_equal type_x constr:(Prop) with
-  | true => throw err_msg
-  | false => 
-    match check_constr_equal type_x constr:(Set) with
-    | true => throw err_msg
-    | false => 
-      match check_constr_equal type_x constr:(Type) with
-      | true => throw err_msg
-      | false => ()
-      end
-    end
+  match! type_x with
+  | Prop => throw err_msg
+  | Set => throw err_msg
+  | Type => throw err_msg
+  | _ => ()
   end.