diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 17:18:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 17:18:58 +0200 |
| commit | dbada2989e334756971c7bf69578c93b2e45643e (patch) | |
| tree | 9ee0e5de226b95f7ac0795ee1018e666a27fc897 /theories/Reals | |
| parent | 332f092e3a30f8428b28f12c85c0a90e3f6d7171 (diff) | |
- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
Diffstat (limited to 'theories/Reals')
0 files changed, 0 insertions, 0 deletions