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.

19 files changed, 133 insertions, 99 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e7d4b605c7..491a75bb3d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -72,6 +72,12 @@ Libobject
   * `Libobject.superglobal_object`
   * `Libobject.superglobal_object_nodischarge`
 
+Implicit Arguments
+
+- `Impargs.declare_manual_implicits` is restricted to only support declaration
+  of implicit binders at constant declaration time. `Impargs.set_implicits` should
+  be used for redeclaration of implicit arguments.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f1733a5ebf..8b7e5c9a02 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1651,6 +1651,13 @@ Declaring Implicit Arguments
    To know which are the implicit arguments of an object, use the
    command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
+.. warn:: Argument number @num is a trailing implicit so must be maximal.
+
+   For instance in
+
+   .. coqtop:: all
+
+      Arguments prod _ [_].
 
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 6fd52d98dd..0646913f96 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -674,7 +674,7 @@ let check_inclusion l =
 	  user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
 	aux nl
     | _ -> () in
-  aux (List.map (fun (imps,_) -> List.length imps) l)
+  aux (List.map snd l)
 
 let check_rigidity isrigid =
   if not isrigid then
@@ -685,6 +685,8 @@ let projection_implicits env p impls =
   CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
+  assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l);
+  assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l);
   let flags = !implicit_args in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -692,29 +694,71 @@ let declare_manual_implicits local ref ?enriching l =
   let t = of_constr t in
   let enriching = Option.default flags.auto enriching in
   let autoimpls = compute_auto_implicits env sigma flags enriching t in
+  let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
+  let req =
+    if is_local local ref then ImplLocal
+    else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
+  in add_anonymous_leaf (inImplicits (req,[ref,l]))
+
+let maybe_declare_manual_implicits local ref ?enriching l =
+  match l with
+  | [] -> ()
+  | _ -> declare_manual_implicits local ref ?enriching l
+
+(* TODO: either turn these warnings on and document them, or handle these cases sensibly *)
+
+let warn_set_maximal_deprecated =
+  CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated"
+    (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal"))
+
+type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
+
+let compute_implicit_statuses autoimps l =
+  let rec aux i = function
+    | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+    | Name id :: autoimps, MaximallyImplicit :: manualimps ->
+       Some (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+    | Name id :: autoimps, Implicit :: manualimps ->
+       let imps' = aux (i+1) (autoimps, manualimps) in
+       let max = set_maximality imps' false in
+       if max then warn_set_maximal_deprecated i;
+       Some (id, Manual, (max, true)) :: imps'
+    | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
+       user_err ~hdr:"set_implicits"
+         (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
+    | autoimps, [] -> List.map (fun _ -> None) autoimps
+    | [], _::_ -> assert false
+  in aux 0 (autoimps, l)
+
+let set_implicits local ref l =
+  let flags = !implicit_args in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let t, _ = Typeops.type_of_global_in_context env ref in
+  let t = of_constr t in
+  let autoimpls = compute_implicits_names env sigma t in
   let l' = match l with
     | [] -> assert false
     | [l] ->
-       [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l]
+       [DefaultImpArgs, compute_implicit_statuses autoimpls l]
     | _ ->
        check_rigidity (is_rigid env sigma t);
-       let l = List.map (fun imps -> (imps,List.length imps)) l in
+       (* Sort by number of implicits, decreasing *)
+       let is_implicit = function
+         | NotImplicit -> false
+         | _ -> true in
+       let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
        let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
        check_inclusion l;
        let nargs = List.length autoimpls in
        List.map (fun (imps,n) ->
            (LessArgsThan (nargs-n),
-            set_manual_implicits flags enriching autoimpls imps)) l in
+            compute_implicit_statuses autoimpls imps)) l in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
   in add_anonymous_leaf (inImplicits (req,[ref,l']))
 
-let maybe_declare_manual_implicits local ref ?enriching l =
-  match l with
-  | [] -> ()
-  | _ -> declare_manual_implicits local ref ?enriching [l]
-
 let extract_impargs_data impls =
   let rec aux p = function
     | (DefaultImpArgs, imps)::_ -> [None,imps]
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 43c26b024f..0070423530 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -112,13 +112,20 @@ val declare_implicits : bool -> GlobRef.t -> unit
    Unsets implicits if [l] is empty. *)
 
 val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
-  manual_implicits list -> unit
+  manual_implicits -> unit
 
 (** If the list is empty, do nothing, otherwise declare the implicits. *)
 
 val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits -> unit
 
+type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
+
+(** [set_implicits local ref l]
+   Manual declaration of implicit arguments.
+  `l` is a list of possible sequences of implicit statuses. *)
+val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit
+
 val implicits_of_global : GlobRef.t -> implicits_list list
 
 val extract_impargs_data :
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.
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index dba72337b2..f5d13053b1 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1789,5 +1789,5 @@ End Field.
 
 End Complete.
 
-Arguments FEO [C].
-Arguments FEI [C].
+Arguments FEO {C}.
+Arguments FEI {C}.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9ef24144d2..12f716c496 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1507,5 +1507,5 @@ Qed.
 
 End MakeRingPol.
 
-Arguments PEO [C].
-Arguments PEI [C].
+Arguments PEO {C}.
+Arguments PEI {C}.
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index ed4ff2aa66..d6b7371647 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -813,21 +813,21 @@ Proof. by case b1; case b2; constructor; auto. Qed.
 
 End ReflectConnectives.
 
-Arguments idP [b1].
-Arguments idPn [b1].
-Arguments negP [b1].
-Arguments negPn [b1].
-Arguments negPf [b1].
-Arguments andP [b1 b2].
-Arguments and3P [b1 b2 b3].
-Arguments and4P [b1 b2 b3 b4].
-Arguments and5P [b1 b2 b3 b4 b5].
-Arguments orP [b1 b2].
-Arguments or3P [b1 b2 b3].
-Arguments or4P [b1 b2 b3 b4].
-Arguments nandP [b1 b2].
-Arguments norP [b1 b2].
-Arguments implyP [b1 b2].
+Arguments idP {b1}.
+Arguments idPn {b1}.
+Arguments negP {b1}.
+Arguments negPn {b1}.
+Arguments negPf {b1}.
+Arguments andP {b1 b2}.
+Arguments and3P {b1 b2 b3}.
+Arguments and4P {b1 b2 b3 b4}.
+Arguments and5P {b1 b2 b3 b4 b5}.
+Arguments orP {b1 b2}.
+Arguments or3P {b1 b2 b3}.
+Arguments or4P {b1 b2 b3 b4}.
+Arguments nandP {b1 b2}.
+Arguments norP {b1 b2}.
+Arguments implyP {b1 b2}.
 Prenex Implicits idP idPn negP negPn negPf.
 Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
 
@@ -953,7 +953,7 @@ Proof. by case: a; case: b. Qed.
 
 Lemma addbP a b : reflect (~~ a = b) (a (+) b).
 Proof. by case: a; case: b; constructor. Qed.
-Arguments addbP [a b].
+Arguments addbP {a b}.
 
 (**
  Resolution tactic for blindly weeding out common terms from boolean
@@ -1158,8 +1158,8 @@ Definition clone_pred U :=
 
 End Predicates.
 
-Arguments pred0 [T].
-Arguments predT [T].
+Arguments pred0 {T}.
+Arguments predT {T}.
 Prenex Implicits pred0 predT predI predU predC predD preim relU.
 
 Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B))
@@ -1357,7 +1357,7 @@ Variant qualifier (q : nat) T := Qualifier of predPredType T.
 
 Coercion has_quality n T (q : qualifier n T) : pred_class :=
   fun x => let: Qualifier _ p := q in p x.
-Arguments has_quality n [T].
+Arguments has_quality n {T}.
 
 Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d083d34b52..2e1554d496 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -152,7 +152,7 @@ let declare_one_prenex_implicit locality f =
     with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
   let rec loop = function
   | a :: args' when Impargs.is_status_implicit a ->
-    (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
+    Impargs.MaximallyImplicit :: loop args'
   | args' when List.exists Impargs.is_status_implicit args' ->
       errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
   | _ -> [] in
@@ -165,7 +165,7 @@ let declare_one_prenex_implicit locality f =
   | [] ->
     errorstrm (str "Expected some implicits for " ++ pr_qualid f)
   | impls ->
-    Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
+    Impargs.set_implicits locality fref [impls]
 
 }
 
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.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index af9050da29..a48e9929c4 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1033,7 +1033,7 @@ Lemma map_ext_in_iff :
    forall (A B : Type)(f g:A->B) l, map f l = map g l <-> forall a, In a l -> f a = g a.
 Proof. split; [apply ext_in_map | apply map_ext_in]. Qed.
 
-Arguments map_ext_in_iff [A B f g l].
+Arguments map_ext_in_iff {A B f g l}.
 
 Lemma map_ext :
   forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
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]"]