Complete rewrite in Ltac2

• Ltac2 gives performances, and better warnings.
• The set of features stays roughly the same, except for users that use the customization tactics (for auto-naming mostly): customization tactics must now be written in Ltac2.
• (experimental) tactic: assert premise i of h.
• See CHANGES.md and README.md for details

4.0.0

This is the first release of rocq-libhyps, adapted from coq-libhyps (which is now only for coq < 9 version and will not be developped anymore).

3.0.2

This release fixes a few bugs in especialize. It is also the first coq < 9 release. It will not evolve much in the future as we focus on rocq >= 9 from now on.

Fix especialize (backward incompatible with 2.x)

3.0.1

udpate opam file to support coq-8.21~

Restoring especialize in an non backward compatible way

First version working around coq 8.19 specialize semantic change wrt evars.

LibHyps 2.0.8

Fixing github actions for tests.

LibHyps 2.0.7

Removing (hopefully temporarily) the especialize tactic, due to an incompatibility with coq-8.18.

License changed fully to MIT

License changed fully to MIT.

LibHyps 2.0.3

Coq opam package license change only.

LibHyps 2.0.2

• bug fixes
• Adding the following options to especialize:

especialize H at *. (* create a subgoal for each (dependent) premise of H. Cf "exploit" from CompCert. *)
especialize H at 2,3,4 (* up to 7 premise number *)
especialize H until 3 (* create goals for the n first (dependent) premises of H. *)

Many thanks to Sylvain Boulmé for the suggestions.