Fixing superflous newline in output of About when no parameter is renamed.

Fixing output tests after having added flushing of warning in
revisions 14747 and 14750.
Moving Implicit output test to new command Arguments.
Adding test of new Arguments syntax in PrintInfos.v.

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

5 files changed, 50 insertions, 10 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3151fa6d07..e30979bf9b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -120,7 +120,7 @@ let print_impargs_list prefix l =
 	    else [str "No implicit arguments"]))])]) l)
 
 let print_renames_list prefix l =
-  if l = [] then [prefix] else
+  if l = [] then [] else
   [add_colon prefix ++ str "Arguments are renamed to " ++
     hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
 
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index c95f89c9f0..756e8ede9a 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -21,6 +21,11 @@ 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
@@ -54,8 +59,3 @@ negb'' : bool -> bool
 
 negb'' is transparent
 Expands to: Constant Top.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
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index d50c98765f..7c9b89f9d2 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -36,7 +36,7 @@ Check map id (1::nil).
 
 Definition id' (A:Type) (x:A) := x.
 
-Implicit Arguments id' [[A]].
+Arguments id' {A} x.
 
 Check map id' (1::nil).
 
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index a2e6a1cfbb..40c786abf5 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -56,6 +56,15 @@ 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
+
+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 _]
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
@@ -69,6 +78,20 @@ 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
+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
 bar : foo
 
 Expanded type for implicit arguments
@@ -85,6 +108,16 @@ 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
+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 _]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
@@ -94,6 +127,3 @@ 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 _]
-Warning: Implicit Arguments is deprecated; use Arguments instead
-Warning: Implicit Arguments is deprecated; use Arguments instead
-Warning: Implicit Arguments is deprecated; use Arguments instead
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 6a89f88098..deeb1f656b 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -15,6 +15,9 @@ About plus_n_O.
 Implicit Arguments le_S [[n] m].
 Print le_S.
 
+Arguments le_S {n} [m] _. (* Test new syntax *)
+Print le_S.
+
 About comparison.
 Print comparison.
 
@@ -24,8 +27,15 @@ Implicit Arguments bar [x].
 About bar.
 Print bar.
 
+Arguments bar [x]. (* Test new syntax *)
+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 *)
+Print eq_refl.