diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
| commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
| tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/bugs/closed/3321.v | |
| parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3321.v')
| -rw-r--r-- | test-suite/bugs/closed/3321.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3321.v b/test-suite/bugs/closed/3321.v index 07e3b3cb..b6f10e53 100644 --- a/test-suite/bugs/closed/3321.v +++ b/test-suite/bugs/closed/3321.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5302 lines to 4649 lines, then from 4660 lines to 355 lines, then from 360 lines to 269 lines, then from 269 lines to 175 lines, then from 144 lines to 119 lines, then from 103 lines to 83 lines, then from 86 lines to 36 lines, then from 37 lines to 17 lines *) Axiom admit : forall {T}, T. |