diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-12 10:58:26 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-31 11:27:15 +0200 |
| commit | 96bbe0590417d8885ac09abf7d749c12172e16bc (patch) | |
| tree | 75e19acb72216ea2784a5464133032638d78dbaf /CHANGES | |
| parent | 0e37dc665cf7a6a9ed7d0d10199dd40134cf0148 (diff) | |
Tests for new specialize feature + CHANGES.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -6,6 +6,9 @@ Tactics - New tactic "extensionality in H" which applies (possibly dependent) functional extensionality in H supposed to be a quantified equality until giving a bare equality. +- Tactic "specialize with ..." now accepts any partial bindings. + Missing bindings are either solved by unification or left quantified + in the hypothesis. - New representation of terms that statically ensure stability by evar-expansion. This has several consequences. * In terms of performance, this adds a cost to every term destructuration, |