aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_123.v
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-05-01 11:34:00 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-05-01 11:34:00 -0400
commitf6856c5022ef27cdc492daadd1301cfcad025b01 (patch)
treee886b9ef6667a23460c72b581481b227336b7128 /test-suite/bugs/closed/HoTT_coq_123.v
parent68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (diff)
remove unneeded -emacs flag to coq-prog-args
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_123.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_123.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index 6ee6e6532..cd9cad406 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -1,5 +1,5 @@
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 original input, then from 4988 lines to 856 lines, then from 648 lines to 398 lines, then from 401 lines to 332 lines, then from 287 lines to 250 lines, then from 257 lines to 241 lines, then from 223 lines to 175 lines *)
Set Universe Polymorphism.
Set Asymmetric Patterns.