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


From 741f3fab052b91eaec57f32b639ca722c3d8dc34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Mar 2017 13:18:42 +0100
Subject: A fix for #5390 (a useful error on used introduction names was
 masked).

With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.
---
 test-suite/output/Tactics.out |  4 ++++
 test-suite/output/Tactics.v   | 10 ++++++++++
 2 files changed, 14 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 239edd1da3..19c9fc4423 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -2,3 +2,7 @@ Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
           | |- context [ if ?X then _ else _ ] => case X
           end
+The command has indeed failed with message:
+H is already used.
+The command has indeed failed with message:
+H is already used.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index a7c497cfaf..9a5edb813d 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -11,3 +11,13 @@ Print Ltac f.
 
 Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
 Print Ltac g.
+
+(* Test an error message (#5390) *)
+Lemma myid (P : Prop) : P <-> P.
+Proof. split; auto. Qed.
+
+Goal True -> (True /\ True) -> True.
+Proof.
+intros H.
+Fail intros [H%myid ?].
+Fail destruct 1 as [H%myid ?].
-- 
cgit v1.2.3


From ac333e6297bd7c32282fa5f47bebeb35826072df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 20 May 2017 01:24:46 +0200
Subject: [test-suite] Add tests for goal printing.

- https://coq.inria.fr/bugs/show_bug.cgi?id=5529
- https://coq.inria.fr/bugs/show_bug.cgi?id=5537

See also PR #640
---
 test-suite/output/goal_output.out |  8 ++++++++
 test-suite/output/goal_output.v   | 13 +++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test-suite/output/goal_output.out
 create mode 100644 test-suite/output/goal_output.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
new file mode 100644
index 0000000000..773533a8d3
--- /dev/null
+++ b/test-suite/output/goal_output.out
@@ -0,0 +1,8 @@
+Nat.t = nat
+     : Set
+Nat.t = nat
+     : Set
+1 subgoal
+  
+  ============================
+  False
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
new file mode 100644
index 0000000000..327b80b0aa
--- /dev/null
+++ b/test-suite/output/goal_output.v
@@ -0,0 +1,13 @@
+(* From
+   - https://coq.inria.fr/bugs/show_bug.cgi?id=5529
+   - https://coq.inria.fr/bugs/show_bug.cgi?id=5537
+ *)
+
+Print Nat.t.
+Timeout 1 Print Nat.t.
+
+Lemma toto: False.
+Set Printing All.
+Show.
+Abort.
+
-- 
cgit v1.2.3


From 04c532d81f69f0b6371b30b524b7aa258a6309c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 17:07:29 +0200
Subject: Added a test for #4765 (an example of printing abbreviation with
 binders).

---
 test-suite/output/Notations3.out | 2 ++
 test-suite/output/Notations3.v   | 5 +++++
 2 files changed, 7 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 360f379676..4d59a92cbf 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,3 +98,5 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
 tele (t : Type) '(y, z) (x : t0) := tt
      : forall t : Type, nat * nat -> t -> fpack
+foo5 x nat x
+     : nat -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 4b8bfe3124..96d831944f 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -139,3 +139,8 @@ Notation "'tele' x .. z := b" :=
   (at level 85, x binder, z binder).
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
+
+(* Cyprien's part of bug #4765 *)
+
+Notation foo5 x T y := (fun x : T => y).
+Check foo5 x nat x.
-- 
cgit v1.2.3