diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 16:04:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 16:04:53 +0200 |
| commit | 42555d7652dde022f63ed6a8e42208b7b360918f (patch) | |
| tree | 503efcc035870a39e7e5c7b9e93ef9b45e41e671 /CHANGES | |
| parent | 11c1d469fc12e617d0840700bc01caf2a1d5276c (diff) | |
| parent | 96bbe0590417d8885ac09abf7d749c12172e16bc (diff) | |
Merge PR#449: make specialize smarter (bug 5370).
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, |