diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-17 17:57:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-17 17:58:11 +0200 |
| commit | d1052e2d9e14684db1f86a9b419d388a8e70728c (patch) | |
| tree | 676d4e684aa65ba6c1d3fd47ba39fb2a530b7541 /CHANGES | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Documenting fix of #3070 (subst and chain of dependencies).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -13,6 +13,7 @@ Bugfixes - #4592, #4932: notations sharing recursive patterns or sharing binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #3070: fixing "subst" in the presence of a chain of dependencies. Specification language |