diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-17 12:17:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-17 12:17:35 +0200 |
| commit | 8beb75435a3ffd3c91ad08cd8b2ca42fb2bb5896 (patch) | |
| tree | 40fafe5a55bff8705cbae1c05f3119b4165c98c7 /test-suite/bugs/closed/4527.v | |
| parent | e09a8cf6a2db97b75796a54296683fe12977d018 (diff) | |
| parent | c64a28ee5a6643449f7c77ed7b8737e8f01ede52 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'test-suite/bugs/closed/4527.v')
| -rw-r--r-- | test-suite/bugs/closed/4527.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index c6fcc24b6..117d6523a 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_bad_univ_length_01") -*- *) (* File reduced by coq-bug-finder from original input, then from 1199 lines to 430 lines, then from 444 lines to 430 lines, then from 964 lines to 255 lines, then from 269 lines to 255 lines *) |