Fix issues in test-suite revealed by warnings.

7 files changed, 13 insertions, 52 deletions

diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v
index 5a7ae2002..d4ce050c5 100644
--- a/test-suite/bugs/closed/3251.v
+++ b/test-suite/bugs/closed/3251.v
@@ -1,4 +1,5 @@
 Goal True.
+idtac.
 Ltac foo := idtac.
 (* print out happens twice:
 foo is defined
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 1ff53294e..3a90cb79d 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -11,11 +11,11 @@ About b.
 About negb''.
 About negb'.
 About negb.
-Global Arguments Scope negb'' [ _ ].
-Global Arguments Scope negb' [ _ ].
-Global Arguments Scope negb [ _ ].
-Global Arguments Scope a [ _ ].
-Global Arguments Scope b [ _ ].
+Global Arguments negb'' _ : clear scopes.
+Global Arguments negb' _ : clear scopes.
+Global Arguments negb _ : clear scopes.
+Global Arguments a _ : clear scopes.
+Global Arguments b _ : clear scopes.
 About a.
 About b.
 About negb.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index e68fbd69f..b6fbeb6ec 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,6 +1,6 @@
 Fail Arguments eq_refl {B y}, [B] y.
 Fail Arguments identity T _ _.
-Arguments eq_refl A x.
+Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
 Check @eq_refl.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index a4d19d693..3c2eaf42c 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -66,8 +66,8 @@ Print foo'.
 (* Was bug #3293 (eta-expansion at "match" printing time was failing because
    of let-in's interpreted as being part of the expansion)  *)
 
-Variable b : bool.
-Variable P : bool -> Prop.
+Axiom b : bool.
+Axiom P : bool -> Prop.
 Inductive B : Prop := AC : P b -> B.
 Definition f : B -> True.
 
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adba688e6..2ccca829d 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -133,8 +133,7 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
 Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
 
 (* Right-unbound variable *)
-(* Now allowed with an only parsing restriction *)
-Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..) (only parsing).
 
 (* Not the right kind of recursive pattern *)
 Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 98420409e..1307a8f26 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -66,14 +66,6 @@ For le_S: Argument n is implicit and maximally inserted
 For le: Argument scopes are [nat_scope nat_scope]
 For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
-Inductive le (n : nat) : nat -> Prop :=
-    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
-
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
 Expands to: Inductive Coq.Init.Datatypes.comparison
@@ -92,19 +84,6 @@ Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
-bar : foo
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
-Expands to: Constant Top.bar
-*** [ bar : foo ]
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
@@ -117,15 +96,6 @@ For eq_refl, when applied to 1 argument:
   Argument A is implicit and maximally inserted
 For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
-
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 3c623346b..08918981a 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -12,10 +12,7 @@ Print Implicit Nat.add.
 
 About plus_n_O.
 
-Implicit Arguments le_S [[n] m].
-Print le_S.
-
-Arguments le_S {n} [m] _. (* Test new syntax *)
+Arguments le_S {n} [m] _.
 Print le_S.
 
 About comparison.
@@ -23,21 +20,15 @@ Print comparison.
 
 Definition foo := forall x, x = 0.
 Parameter bar : foo.
-Implicit Arguments bar [x].
-About bar.
-Print bar.
 
-Arguments bar [x]. (* Test new syntax *)
+Arguments bar [x].
 About bar.
 Print bar.
 
 About Peano. (* Module *)
 About existS2. (* Notation *)
 
-Implicit Arguments eq_refl [[A] [x]] [[A]].
-Print eq_refl.
-
-Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *)
+Arguments eq_refl {A} {x}, {A} x.
 Print eq_refl.