diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-12 17:13:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-12 17:16:44 +0200 |
| commit | 8a6c792505160de4ba2123ef049ab45d28873e47 (patch) | |
| tree | 356a9bcbe40d3fc81be7607e868dac904a0b80a8 /CHANGES | |
| parent | 1a9fe0dfe837ccbee25e9ecf19a7b2e7768a7958 (diff) | |
Allocating a section in CHANGES for changes specific to 8.7.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 11 |
1 files changed, 10 insertions, 1 deletions
@@ -1,6 +1,15 @@ -Changes beyond V8.5 +Changes beyong V8.6 =================== +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. + +Changes from V8.5 to V8.6beta1 +============================== + Bugfixes - #4527: when typechecking the statement of a lemma using universe polymorphic |