10 files changed, 59 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 2ccca829d6..b9985a594f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -1,3 +1,14 @@
+(* Bug 5568, don't warn for notations in repeated module import *)
+
+Module foo.
+Notation compose := (fun g f => g f).
+Notation "g & f" := (compose g f) (at level 10).
+End foo.
+
+Import foo.
+Import foo.
+Import foo.
+
 (**********************************************************************)
 (* Notations for if and let (submitted by Roland Zumkeller)           *)
 
diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.out
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
new file mode 100644
index 0000000000..cd667bbd00
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -0,0 +1,5 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+
+(* Test that mentioning a warning defined in plugins works. The failure
+mode here is that these result in a warning about unknown warnings, since the
+plugins are not known at command line parsing time. *)
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
new file mode 100644
index 0000000000..73369ab713
--- /dev/null
+++ b/test-suite/output/TypeclassDebug.out
@@ -0,0 +1,18 @@
+Debug: 1: looking for foo without backtracking
+Debug: 1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2 : foo
+Debug: 1.1-2: looking for foo without backtracking
+Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2 : foo
+Debug: 1.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2 : foo
+Debug: 1.1-2.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2.1-2 : foo
+Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo
+The command has indeed failed with message:
+Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
+Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
new file mode 100644
index 0000000000..d38e2a50e4
--- /dev/null
+++ b/test-suite/output/TypeclassDebug.v
@@ -0,0 +1,8 @@
+(* show alternating separators in typeclass debug output; see discussion in PR #868 *)
+
+Parameter foo : Prop.
+Axiom H : foo -> foo.
+Hint Resolve H : foo.
+Goal foo.
+Typeclasses eauto := debug.
+Fail typeclasses eauto 5 with foo.
diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out
new file mode 100644
index 0000000000..47409f3ec5
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.out
@@ -0,0 +1 @@
+type foo = __
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
new file mode 100644
index 0000000000..c6e0054641
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
+
+Require Extraction.
+Axiom foo : Prop.
+
+Extraction foo.
+
diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
new file mode 100644
index 0000000000..a70f8ca45a
--- /dev/null
+++ b/test-suite/output/Warnings.out
@@ -0,0 +1,3 @@
+File "stdin", line 4, characters 0-22:
+Warning: Projection value has no head constant: fun x : B => x in canonical
+instance a of b, ignoring it. [projection-no-head-constant,typechecker]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
new file mode 100644
index 0000000000..7465442cab
--- /dev/null
+++ b/test-suite/output/Warnings.v
@@ -0,0 +1,5 @@
+(* Term in warning was not printed in the right environment at some time *)
+Record A := { B:Type; b:B->B }.
+Definition a B := {| B:=B; b:=fun x => x |}.
+Canonical Structure a.
+
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index f761a4dc5a..73169dae65 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Warnings Append "-deprecated-option".
 Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).