diff options
Diffstat (limited to 'test-suite/bugs/closed/3329.v')
| -rw-r--r-- | test-suite/bugs/closed/3329.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3329.v b/test-suite/bugs/closed/3329.v index f7e368f8..ecb09e84 100644 --- a/test-suite/bugs/closed/3329.v +++ b/test-suite/bugs/closed/3329.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12095 lines to 869 lines, then from 792 lines to 504 lines, then from 487 lines to 353 lines, then from 258 lines to 174 lines, then from 164 lines to 132 lines, then from 129 lines to 99 lines *) Set Universe Polymorphism. Generalizable All Variables. |