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/HoTT_coq_107.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs/closed/HoTT_coq_107.v') diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index 7c1ab8dc2..fa4072a8f 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. -- cgit v1.2.3