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.

7 files changed, 26 insertions, 57 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 263ebf5f5a..453b863be6 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
   if program_mode then
     let hook _ _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-      Impargs.declare_manual_implicits false gr [imps];
+      Impargs.declare_manual_implicits false gr imps;
       let pri = intern_info pri in
       Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
     in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index cc9c83bd17..ae77cf12e5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -215,7 +215,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
-          Impargs.declare_manual_implicits false gr [impls]
+          Impargs.declare_manual_implicits false gr impls
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
       hook, name, typ
@@ -223,7 +223,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
       let hook sigma _ _ l gr =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
-          Impargs.declare_manual_implicits false gr [impls]
+          Impargs.declare_manual_implicits false gr impls
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42bee25da3..589b15fd41 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,6 +16,7 @@ open Util
 open Names
 open Glob_term
 open Vernacexpr
+open Impargs
 open Constrexpr
 open Constrexpr_ops
 open Extend
@@ -836,11 +837,11 @@ GRAMMAR EXTEND Gram
   ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> { [(name.CAst.v, Vernacexpr.NotImplicit)] }
+    [ name = name -> { [(name.CAst.v, NotImplicit)] }
     | "["; items = LIST1 name; "]" ->
-       { List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items }
+       { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
     | "{"; items = LIST1 name; "}" ->
-       { List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items }
+       { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
     ]
   ];
   strategy_level:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d22e52e960..f705f347a3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1033,9 +1033,9 @@ open Pputils
               let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
               let pr_if b x = if b then x else str "" in
               let pr_br imp x = match imp with
-                | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
-                | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
-                | Vernacexpr.NotImplicit -> x in
+                | Impargs.Implicit -> str "[" ++ x ++ str "]"
+                | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
+                | Impargs.NotImplicit -> x in
               let rec print_arguments n l =
                 match n, l with
                   | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
diff --git a/vernac/record.ml b/vernac/record.ml
index 0bd15e203b..9c52ac4ee5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -487,8 +487,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
         (DefinitionEntry proj_entry, IsDefinition Definition)
       in
       let cref = ConstRef cst in
-      Impargs.declare_manual_implicits false cref [paramimpls];
-      Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+      Impargs.declare_manual_implicits false cref paramimpls;
+      Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
 	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 11b64a5247..9e345da57d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1173,14 +1173,6 @@ let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";
   Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
 
-let vernac_declare_implicits ~section_local r l =
-  match l with
-  | [] ->
-      Impargs.declare_implicits section_local (smart_global r)
-  | _::_ as imps ->
-      Impargs.declare_manual_implicits section_local (smart_global r) ~enriching:false
-	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
-
 let warn_arguments_assert =
   CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
          (fun sr ->
@@ -1336,43 +1328,15 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
     user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
   end;
 
-  (* Parts of this code are overly complicated because the implicit arguments
-     API is completely crazy: positions (ExplByPos) are elaborated to
-     names. This is broken by design, since not all arguments have names. So
-     even though we eventually want to map only positions to implicit statuses,
-     we have to check whether the corresponding arguments have names, not to
-     trigger an error in the impargs code. Even better, the names we have to
-     check are not the current ones (after previous renamings), but the original
-     ones (inferred from the type). *)
-
   let implicits =
     List.map (fun { name; implicit_status = i } -> (name,i)) args
   in
   let implicits = implicits :: more_implicits in
 
-  let open Vernacexpr in
-  let rec build_implicits inf_names implicits =
-    match inf_names, implicits with
-    | _, [] -> []
-    | _ :: inf_names, (_, NotImplicit) :: implicits ->
-       build_implicits inf_names implicits
-
-    (* With the current impargs API, it is impossible to make an originally
-       anonymous argument implicit *)
-    | Anonymous :: _, (name, _) :: _ ->
-       user_err ~hdr:"vernac_declare_arguments"
-                    (strbrk"Argument "++ Name.print name ++ 
-                       strbrk " cannot be declared implicit.")
-
-    | Name id :: inf_names, (name, impl) :: implicits ->
-       let max = impl = MaximallyImplicit in
-       (ExplByName id,max,false) :: build_implicits inf_names implicits
-    
-    | _ -> assert false (* already checked in [names_union] *)
-  in
-  
-  let implicits = List.map (build_implicits inf_names) implicits in
-  let implicits_specified = match implicits with [[]] -> false | _ -> true in
+  let implicits = List.map (List.map snd) implicits in
+  let implicits_specified = match implicits with
+    | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+    | _ -> true in
 
   if implicits_specified && clear_implicits_flag then
     user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
@@ -1415,10 +1379,10 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
     end;
 
   if implicits_specified || clear_implicits_flag then
-    vernac_declare_implicits ~section_local reference implicits;
+    Impargs.set_implicits section_local (smart_global reference) implicits;
 
   if default_implicits_flag then
-    vernac_declare_implicits ~section_local reference [];
+    Impargs.declare_implicits section_local (smart_global reference);
 
   if red_modifiers_specified then begin
     match sr with
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2eb901890b..d1da7c0602 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -237,13 +237,11 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
 
 (** {6 The type of vernacular expressions} *)
 
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
 type vernac_argument_status = {
   name : Name.t;
   recarg_like : bool;
   notation_scope : string CAst.t option;
-  implicit_status : vernac_implicit_status;
+  implicit_status : Impargs.implicit_kind;
 }
 
 type extend_name =
@@ -355,7 +353,7 @@ type nonrec vernac_expr =
       onlyparsing_flag
   | VernacArguments of qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
-        (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
+        (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
         [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
           `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
@@ -409,3 +407,9 @@ type vernac_control =
   | VernacRedirect of string * vernac_control CAst.t
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
+
+(** Deprecated *)
+
+type vernac_implicit_status = Impargs.implicit_kind =
+  | Implicit [@ocaml.deprecated] | MaximallyImplicit [@ocaml.deprecated] | NotImplicit [@ocaml.deprecated]
+[@@ocaml.deprecated "Use [Impargs.implicit_kind]"]