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/3263.v | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'test-suite/bugs/opened/3263.v')
| -rw-r--r-- | test-suite/bugs/opened/3263.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v index 6de13f74..f0c707bd 100644 --- a/test-suite/bugs/opened/3263.v +++ b/test-suite/bugs/opened/3263.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) Generalizable All Variables. Set Implicit Arguments. |