Fixing some tests from the test-suite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 9 insertions, 13 deletions

diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 756e8ede9a..6643c1429a 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -21,11 +21,6 @@ negb : bool -> bool
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
-Warning: Arguments Scope is deprecated; use Arguments instead
 a : bool -> bool
 
 Expands to: Variable a
diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out
index 951a98db0e..8b13725996 100644
--- a/test-suite/output/Match_subterm.out
+++ b/test-suite/output/Match_subterm.out
@@ -1,4 +1,6 @@
 (0 = 1)
+(eq 0)
+eq
 eq
 nat
 0
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 23f33081b4..b3914a1cc4 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -2,6 +2,8 @@ Axioms:
 foo : nat
 Axioms:
 foo : nat
+Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Arith/Plus.vo
+Fetching opaque terms in /home/pm/Desktop/sources/coq/theories/Init/Peano.vo
 Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 7bddcc6784..e0fb7d5a95 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -57,7 +57,6 @@ plus_n_O : forall n : nat, n = n + 0
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
-Warning: Implicit Arguments is deprecated; use Arguments instead
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
@@ -79,7 +78,6 @@ comparison : Set
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
-Warning: Implicit Arguments is deprecated; use Arguments instead
 bar : foo
 
 Expanded type for implicit arguments
@@ -109,7 +107,6 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
-Warning: Implicit Arguments is deprecated; use Arguments instead
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index ea7ce12662..2892dfd5a1 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -1,6 +1,6 @@
 The command has indeed failed with message:
 => Error:
-   In environment
-   y : nat
-   The term "a y" has type "{y0 : nat | y = y0}"
-   while it is expected to have type "{x : nat | x = y}".
+In environment
+y : nat
+The term "a y" has type "{y0 : nat | y = y0}"
+while it is expected to have type "{x : nat | x = y}".
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index 551e0ecbcd..bfddd84682 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -16,7 +16,7 @@ Definition π₂ := snd.
 (** More unicode in identifiers *)
 Definition αβ_áà_אב := 0.
 
-Notation "C ᵒᵖ" := C (at level 30).
+Notation "C 'ᵒᵖ'" := C (at level 30).
 
 (** UNICODE IN STRINGS *)