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.

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 751f0d8334..c2dec264ad 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -294,10 +294,10 @@ Qed.
 
 End Store.
 
-Arguments PNone [A].
+Arguments PNone {A}.
 Arguments PSome [A] _.
 
-Arguments Tempty [A].
+Arguments Tempty {A}.
 Arguments Branch0 [A] _ _.
 Arguments Branch1 [A] _ _ _.
 
@@ -311,7 +311,7 @@ Arguments mkStore [A] index contents.
 Arguments index [A] s.
 Arguments contents [A] s.
 
-Arguments empty [A].
+Arguments empty {A}.
 Arguments get [A] i S.
 Arguments push [A] a S.
 
@@ -319,7 +319,7 @@ Arguments get_empty [A] i.
 Arguments get_push_Full [A] i a S _.
 
 Arguments Full [A] _.
-Arguments F_empty [A].
+Arguments F_empty {A}.
 Arguments F_push [A] a S _.
 Arguments In [A] x S F.