- Compatibility with earlier OCaml compilers
- Fixes for the strong induction tactic
- Improve the
Either
tactic: now proves and destructs ordinary 'ors' when the goal is a proposition - Improve some mathematical definitions
- Add vernacular for debugging automation
- Improve errors and warnings
- Rework expanding definitions
- Deal better with Rabs, Rmax, Rmin
- Build the plugin with dune
- 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
- Added and updated theory files.
- Improved notation for (in)equality chains, e.g. (& a < b <= c = d).
- Bug fixes.
- 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.
- Ported the original library written in ltac to Ltac2.