Complete overhaul of the Arguments vernacular.

The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.

The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".

The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.

We also add *a lot* of missing checks on input values and fix various
bugs.

Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.

4 files changed, 15 insertions, 25 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b8c07512f..b99d80e95 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c62..a2ee2d4c8 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra argument _.
+Error: Extra arguments: _, _.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1633ad976..8c5efcd89 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,20 +1,12 @@
-File "stdin", line 1, characters 0-36:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
-Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
-File "stdin", line 2, characters 0-25:
-Warning: This command is just asserting the number and names of arguments of
-identity. If this is what you want add ': assert' to silence the warning. If
-you want to clear implicit arguments add ': clear implicits'. If you want to
-clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
-File "stdin", line 4, characters 0-40:
-Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Warning: This command is just asserting the names of arguments of identity.
+If this is what you want add ': assert' to silence the warning. If you want
+to clear implicit arguments add ': clear implicits'. If you want to clear
+notation scopes add ': clear scopes' [arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -112,18 +104,16 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: All arguments lists must declare the same names.
+Error: Arguments lists should agree on names they provide.
 The command has indeed failed with message:
-Error: The following arguments are not declared: x.
+Error: Sequences of implicit arguments must be of different lengths
 The command has indeed failed with message:
 Error: Arguments names must be distinct.
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-Error: Extra argument y.
-File "stdin", line 53, characters 0-26:
-Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
-[arguments-ignore-rename-nonimpl,vernacular]
+Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+Error: To rename arguments the "rename" flag must be
+specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index e42c98336..2d14c94ac 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Arguments identity T _ _.
+Arguments identity A _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
@@ -46,9 +46,9 @@ About myplus.
 Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
-Fail Arguments eq_refl {F}, [F].
+Fail Arguments eq_refl {F}, [F] : rename.
 Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.