diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-09 19:10:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-09 19:17:03 +0200 |
| commit | 4de7d7fb63a68b766126ae467be1e9bc00b92948 (patch) | |
| tree | 423502e158d2f9cfe17fa71772488862476f53d3 /CHANGES | |
| parent | 5ea2539d4a7d12938787a74a12112e76aaf2a4ee (diff) | |
Reporting about a few bug fixes (to be continued).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -3,8 +3,12 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes -- #4677: fix alpha-conversion in notations needing eta-expansion +- #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. +- #4644: a regression in unification. +- #4777: printing inefficiency with implicit arguments +- #4752: CoqIDE crash on files not ended by ".v". +- #4398: type_scope used consistently in "match goal". Changes from V8.5 to V8.5pl1 ============================ |