summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/HoTT_coq_113.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/HoTT_coq_113.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/HoTT_coq_113.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_113.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/closed/HoTT_coq_113.v
index 3ef531bc..05e76784 100644
--- a/test-suite/bugs/closed/HoTT_coq_113.v
+++ b/test-suite/bugs/closed/HoTT_coq_113.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *)
Generalizable All Variables.