diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:09:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:51:02 +0200 |
| commit | fd0cd480a720cbba15de86bbc9cad74ba6d89675 (patch) | |
| tree | 157da3e6f8a88f752fe516e34d70d58a7864021c /CHANGES | |
| parent | 2042daa9a6e13cbb9636a62812015749d95c2283 (diff) | |
A new step on using alpha-conversion in printing notations.
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -1,5 +1,6 @@ Changes beyond V8.5 =================== + Bugfixes - #4527: when typechecking the statement of a lemma using universe polymorphic @@ -9,6 +10,8 @@ Bugfixes compatible). - #4726: treat user-provided sorts of universe polymorphic records as rigid (i.e. non-minimizable). +- #4592, #4932: notations sharing recursive patterns or sharing + binders made more robust. Specification language |