summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3319.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /test-suite/bugs/closed/3319.v
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3319.v')
-rw-r--r--test-suite/bugs/closed/3319.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3319.v b/test-suite/bugs/closed/3319.v
index bb5853dd..3b37e39e 100644
--- a/test-suite/bugs/closed/3319.v
+++ b/test-suite/bugs/closed/3319.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 5353 lines to 4545 lines, then from 4513 lines to 4504 lines, then from 4515 lines to 4508 lines, then from 4519 lines to 132 lines, then from 111 lines to 66 lines, then from 68 lines to 35 lines *)
Set Implicit Arguments.
Inductive paths {A : Type} (a : A) : A -> Type :=