- 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