diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-17 23:48:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | 4940f99922b0784d726b7c50abe63395713f012f (patch) | |
| tree | 750124bae7b6a575d98b9cfe439c798c555fc531 /vernac/obligations.ml | |
| parent | f8e639f3b81ae142f5b529be1ad90210fc259375 (diff) | |
Fix #5347: unify declaration of axioms with and without bound univs.
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions