diff options
Diffstat (limited to 'test-suite/bugs/closed/3373.v')
| -rw-r--r-- | test-suite/bugs/closed/3373.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v index 5ecf2801..051e6952 100644 --- a/test-suite/bugs/closed/3373.v +++ b/test-suite/bugs/closed/3373.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then |