From f6856c5022ef27cdc492daadd1301cfcad025b01 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 1 May 2017 11:34:00 -0400 Subject: remove unneeded -emacs flag to coq-prog-args --- test-suite/bugs/closed/3352.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/3352.v') diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index f8113e4c7..555accfd5 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty" Defined. Module B. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -- cgit v1.2.3