diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
| commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
| tree | aefad2e3de35f75c46729f9310d33b56d3821961 /test-suite/bugs/closed/3559.v | |
| parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
| parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) | |
Imported Upstream version 8.5~beta3+dfsg
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 50645090..da12b686 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 *) |