Merge branch 'master' into ltac2-hooks

4 files changed, 14 insertions, 2 deletions

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
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.