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/output/ErrorInModule.v  | 2 +-
 test-suite/output/ErrorInSection.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index e69e23276b..b2e3c3e923 100644
--- a/test-suite/output/ErrorInModule.v
+++ b/test-suite/output/ErrorInModule.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
 Module M.
   Definition foo := nonexistent.
 End M.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
index 3036f8f05b..505c5ce378 100644
--- a/test-suite/output/ErrorInSection.v
+++ b/test-suite/output/ErrorInSection.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
 Section S.
   Definition foo := nonexistent.
 End S.
-- 
cgit v1.2.3


From 697cd5a8e7927873ed6700c7e906ae3675bd98b1 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 May 2017 10:30:50 +0200
Subject: Simplified compaction criterion + tests.

---
 test-suite/output/CompactContexts.out | 7 +++++++
 test-suite/output/CompactContexts.v   | 5 +++++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/output/CompactContexts.out
 create mode 100644 test-suite/output/CompactContexts.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/CompactContexts.out b/test-suite/output/CompactContexts.out
new file mode 100644
index 0000000000..9d1d19877e
--- /dev/null
+++ b/test-suite/output/CompactContexts.out
@@ -0,0 +1,7 @@
+1 subgoal
+  
+  hP1 : True
+  a : nat   b : list nat   h : forall x : nat, {y : nat | y > x}
+  h2 : True
+  ============================
+  False
diff --git a/test-suite/output/CompactContexts.v b/test-suite/output/CompactContexts.v
new file mode 100644
index 0000000000..07588d34f9
--- /dev/null
+++ b/test-suite/output/CompactContexts.v
@@ -0,0 +1,5 @@
+Set Printing Compact Contexts.
+
+Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False.
+Show.
+Abort.
\ No newline at end of file
-- 
cgit v1.2.3