Releases: Matafou/LibHyps
Fix especialize (backward incompatible with 2.x)
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.
New syntax - better hyps grouping
2.0.1: fixing the configure script for coq-opam-archive.
2.0.0: This release adds a new syntax for usual post-tactic actions, like /n for autonaming, /s for subst, /g for grouping non-Prop hyps at top, etc. The grouping has been enhanced: it groups hypothesis with similar (non-Prop) types.
New syntax - better hyps grouping
This release adds a new syntax for usual post-tactic actions, like /n for autonaming, /s for subst, /g for grouping non-Prop hyps at top, etc.
The grouping has been enhanced: it groups hypothesis with similar (non-Prop) types.
Small bug fix + demo reworded.
Rare incompatibilities expected.