diff options
| author | Tej Chajed | 2018-02-12 10:44:41 -0500 |
|---|---|---|
| committer | Tej Chajed | 2018-02-13 09:34:19 -0500 |
| commit | 8288e56bbf737cde9eb2e36c3d634a5acbb04b83 (patch) | |
| tree | 15a0da5c0eb659f9d9475c4bc05be4ba15e810e4 | |
| parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
Add CHANGES entry for #1047
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -68,6 +68,8 @@ Universes module and library boundaries. Global universe names introduced in an inductive / constant / Let declaration get qualified with the name of the declaration. +- Fix #5726: Notations that start with `Type` now support universe instances + with `@{u}`. Checker |
