Implement a method for manual declaration of implicits.

This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.

Two disabled warnings are added for things that currently pass silently.

Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.

2 files changed, 3 insertions, 2 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index ba4bc070c6..3f0717666c 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -113,7 +113,8 @@ Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
 Some argument names are duplicated: F
 The command has indeed failed with message:
-Argument z cannot be declared implicit.
+Argument number 2 (anonymous in original definition) cannot be declared
+implicit.
 The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index d7c271c3ec..d95cc0e32f 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -22,7 +22,7 @@ Print comparison.
 Definition foo := forall x, x = 0.
 Parameter bar : foo.
 
-Arguments bar [x].
+Arguments bar {x}.
 About bar.
 Print bar.