diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
| commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
| tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /test-suite/bugs/closed/3393.v | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3393.v')
| -rw-r--r-- | test-suite/bugs/closed/3393.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v index ec25e682..f7ab5f76 100644 --- a/test-suite/bugs/closed/3393.v +++ b/test-suite/bugs/closed/3393.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) Set Universe Polymorphism. |