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/opened/HoTT_coq_120.v | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_120.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_120.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v index 7847c5e4..05ee6c7b 100644 --- a/test-suite/bugs/opened/HoTT_coq_120.v +++ b/test-suite/bugs/opened/HoTT_coq_120.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *) Set Universe Polymorphism. Generalizable All Variables. |