From d1052e2d9e14684db1f86a9b419d388a8e70728c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Aug 2016 17:57:45 +0200 Subject: Documenting fix of #3070 (subst and chain of dependencies). --- CHANGES | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGES b/CHANGES index a9942d3a17..8f873bd91c 100644 --- a/CHANGES +++ b/CHANGES @@ -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 -- cgit v1.2.3