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/3347.v | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3347.v')
| -rw-r--r-- | test-suite/bugs/closed/3347.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 37c0d87e..63d5c7a5 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). |