package coq-waterproof
Install
Dune Dependency
Authors
Maintainers
Sources
md5=a7d2922fb4ed7f0b8fe38074319890fe
sha512=3c511d066ba324cf19fc5620ae89ad09796f3a04576012739783100487dd8d50214edab9bdfc85d581d6538e601511f4563b90ad1dc3041e60a9702f4875e31d
CHANGES.md.html
Change log for the coq-waterproof library
Version 2.1.1+8.18
Compatibility with Coq 8.18
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 propositionImprove some mathematical definitions
Add vernacular for debugging automation
Version 2.0.2+8.17
Improve errors and warnings
Rework expanding definitions
Deal better with Rabs, Rmax, Rmin
Version 2.0.1+8.17
Build the plugin with dune
Version 2.0.0
Converted coq library to coq plugin
Automation procedures are now handled internally in the plugin, so that they can be customized and so that one can check the use of certain lemmas within the automation
Version 1.2.4
Added and updated theory files.
Improved notation for (in)equality chains, e.g. (& a < b <= c = d).
Bug fixes.
Version 1.1.2
Added and updated theory files.
Reorganized automation libraries.
Added goal wrappers that force user to write sentences that make proofscript more readable.
Support chains of (in)equalities for
=
,<
and<=
in naturals and reals.Fixed issues with several tactics, including
Take ...
.Rephrased multiple tactics like
Obtain ... according to ..., ...
.For propositions, have user specify types rather than labels in tactics. Labeling is now optional.
Added some shielding for use of automation, e.g. statements starting with quantifiers cannot be proved automatically.
Version 1.0.0
Ported the original library written in ltac to Ltac2.