aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-09-23 19:14:05 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2015-10-02 15:54:11 +0200
commit43858a207437fa08f066bdd3cae7bcd3034808f1 (patch)
treeabc028574bdfd99b22c348e09b4ccd92c8b5e321 /parsing
parentc92946243ccb0b11cd138f040a5297979229c3f5 (diff)
Univs: fix Universe vernacular, fix bug #4287.
No universe can be set lower than Prop anymore (or Set).
Diffstat (limited to 'parsing')
0 files changed, 0 insertions, 0 deletions