summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3347.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 13:15:50 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 13:15:50 +0200
commite347929583f820a2cc0296597b6382309e930989 (patch)
treecdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/bugs/closed/3347.v
parentc01be74d81a5466c58f8dc6c568db286b0979997 (diff)
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3347.v')
-rw-r--r--test-suite/bugs/closed/3347.v1
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).