diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 13:11:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 13:17:11 +0200 |
| commit | d37aab528dca587127b9f9944e1521e4fc3d9cc7 (patch) | |
| tree | 3d8db828b3e6644c924a75592dded2a168fbeb59 /test-suite/bugs/closed/3559.v | |
| parent | 840155eafd9607c7656c80770de1e2819fe56a13 (diff) | |
Univs: add Strict Universe Declaration option (on by default)
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
Diffstat (limited to 'test-suite/bugs/closed/3559.v')
| -rw-r--r-- | test-suite/bugs/closed/3559.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v index 50645090f..da12b6868 100644 --- a/test-suite/bugs/closed/3559.v +++ b/test-suite/bugs/closed/3559.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 8657 lines to 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines, then from 51 lines to 37 lines, then from 43 lines to 30 lines *) |