diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-05-01 11:34:00 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-05-01 11:34:00 -0400 |
| commit | f6856c5022ef27cdc492daadd1301cfcad025b01 (patch) | |
| tree | e886b9ef6667a23460c72b581481b227336b7128 /test-suite/bugs/closed/HoTT_coq_062.v | |
| parent | 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (diff) | |
remove unneeded -emacs flag to coq-prog-args
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_062.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_062.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index 90d1d1830..e01f73f1b 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,6 +1,6 @@ Unset Strict Universe Declaration. Require Import TestSuite.admit. -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) Set Universe Polymorphism. Definition admit {T} : T. |