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/3382.v | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3382.v')
| -rw-r--r-- | test-suite/bugs/closed/3382.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v index 1d8e9167..3e374d90 100644 --- a/test-suite/bugs/closed/3382.v +++ b/test-suite/bugs/closed/3382.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *) Set Implicit Arguments. |