Merge PR #11235: Add syntax for non maximal implicit arguments

Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes

25 files changed, 238 insertions, 101 deletions

diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
new file mode 100644
index 0000000000..fd63980036
--- /dev/null
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then
+
+    quickchick_CI_REF=non_maximal_implicit
+    quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick
+
+    elpi_CI_REF=non_maximal_implicit
+    elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 3bc92e6aee..cb6e695865 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -17,6 +17,11 @@ Printers:
   Constrextern.extern_constr which were taking a boolean argument for
   the goal style now take instead a label.
 
+Implicit arguments:
+
+- The type `Impargs.implicit_kind` was removed in favor of
+  `Glob_term.binding_kind`.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
new file mode 100644
index 0000000000..d8ff1fec31
--- /dev/null
+++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Syntax for non maximal implicit arguments in definitions and terms using
+  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
+  to be consistent with the command :cmd:`Arguments (implicits)`.
+  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
+  by SimonBoulier).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 510e271951..b3ebb4d8df 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be
 implicitly applied to the implicit arguments it is waiting for: one
 says that the implicit argument is maximally inserted.
 
-Each implicit argument can be declared to have to be inserted maximally or non
-maximally. This can be governed argument per argument by the command
-:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag.
+Each implicit argument can be declared to be inserted maximally or non
+maximally. In Coq, maximally-inserted implicit arguments are written between curly braces
+"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]".
 
-.. seealso:: :ref:`displaying-implicit-args`.
+.. seealso:: :flag:`Maximal Implicit Insertion`
+
+Trailing Implicit Arguments
++++++++++++++++++++++++++++
+
+An implicit argument is considered trailing when all following arguments are declared
+implicit. Trailing implicit arguments cannot be declared non maximally inserted,
+otherwise they would never be inserted.
+
+.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ].
+
+   For instance:
+
+   .. coqtop:: all fail
+
+      Fail Definition double [n] := n + n.
 
 
 Casual use of implicit arguments
@@ -1608,7 +1623,7 @@ Implicit Argument Binders
 In the first setting, one wants to explicitly give the implicit
 arguments of a declared object as part of its definition. To do this,
 one has to surround the bindings of implicit arguments by curly
-braces:
+braces or square braces:
 
 .. coqtop:: all
 
@@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed:
 
    Goal forall A, compose id id = id (A:=A).
 
+For non maximally inserted implicit arguments, use square brackets:
+
+.. coqtop:: all
+
+   Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B :=
+     match l with
+     | nil => nil
+     | cons a t => cons (f a) (map f t)
+     end.
+
+   Print Implicit map.
 
 The syntax is supported in all top-level definitions:
 :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype
@@ -1728,14 +1754,6 @@ Declaring Implicit Arguments
    To know which are the implicit arguments of an object, use the
    command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
-.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ].
-
-   For instance in
-
-   .. coqtop:: all fail
-
-      Arguments prod _ [_].
-
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1811,7 +1829,7 @@ appear strictly in the body of the type, they are implicit.
 
 
 Mode for automatic declaration of implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+++++++++++++++++++++++++++++++++++++++++++++++++++++
 
 .. flag:: Implicit Arguments
 
@@ -1823,7 +1841,7 @@ Mode for automatic declaration of implicit arguments
 .. _controlling-strict-implicit-args:
 
 Controlling strict implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
++++++++++++++++++++++++++++++++++++++
 
 .. flag:: Strict Implicit
 
@@ -1842,7 +1860,7 @@ Controlling strict implicit arguments
 .. _controlling-contextual-implicit-args:
 
 Controlling contextual implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
++++++++++++++++++++++++++++++++++++++++++
 
 .. flag:: Contextual Implicit
 
@@ -1853,7 +1871,7 @@ Controlling contextual implicit arguments
 .. _controlling-rev-pattern-implicit-args:
 
 Controlling reversible-pattern implicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
++++++++++++++++++++++++++++++++++++++++++++++++++
 
 .. flag:: Reversible Pattern Implicit
 
@@ -1864,7 +1882,7 @@ Controlling reversible-pattern implicit arguments
 .. _controlling-insertion-implicit-args:
 
 Controlling the insertion of implicit arguments not followed by explicit arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
 .. flag:: Maximal Implicit Insertion
 
@@ -1873,6 +1891,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen
    function is partially applied and the next argument of the function is
    an implicit one.
 
+Combining manual declaration and automatic declaration
+++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+When some arguments are manually specified implicit with binders in a definition
+and the automatic declaration mode in on, the manual implicit arguments are added to the
+automatically declared ones.
+
+In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off,
+some trailing implicit arguments can be inferred to be non maximally inserted. In
+this case, they are converted to maximally inserted ones.
+
+.. example::
+
+   .. coqtop:: all
+
+      Set Implicit Arguments.
+      Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0.
+      Print Implicit eq0_le0.
+      Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0.
+      Print Implicit eq0_le0'.
+
+
 .. _explicit-applications:
 
 Explicit applications
@@ -2136,8 +2176,10 @@ Implicit generalization
 ~~~~~~~~~~~~~~~~~~~~~~~
 
 .. index:: `{ }
+.. index:: `[ ]
 .. index:: `( )
 .. index:: `{! }
+.. index:: `[! ]
 .. index:: `(! )
 
 Implicit generalization is an automatic elaboration of a statement
@@ -2145,11 +2187,12 @@ with free variables into a closed statement where these variables are
 quantified explicitly.
 
 It is activated for a binder by prefixing a \`, and for terms by
-surrounding it with \`{ } or \`( ).
+surrounding it with \`{ }, or \`[ ] or \`( ).
 
 Terms surrounded by \`{ } introduce their free variables as maximally
-inserted implicit arguments, and terms surrounded by \`( ) introduce
-them as explicit arguments.
+inserted implicit arguments, terms surrounded by \`[ ] introduce them as
+non maximally inserted implicit arguments and terms surrounded by \`( )
+introduce them as explicit arguments.
 
 Generalizing binders always introduce their free variables as
 maximally inserted implicit arguments. The binder itself introduces
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index d591718b17..09090ce89a 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -283,8 +283,10 @@ Binders
    | ( {+ @name } : @term )
    | ( @name {? : @term } := @term )
    | %{ {+ @name } {? : @term } %}
+   | [ {+ @name } {? : @term } ]
    | `( {+, @typeclass_constraint } )
    | `%{ {+, @typeclass_constraint } %}
+   | `[ {+, @typeclass_constraint } ]
    | ' @pattern0
    | ( @name : @term %| @term )
    typeclass_constraint ::= {? ! } @term
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4ae5bf676..b1e12bd66e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -330,15 +330,18 @@ let exists_name na l =
   | _ -> false
 
 let build_impls ?loc n bk na acc =
-  match bk with
-  | Implicit ->
+  let impl_status max =
     let na =
-       if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
-       else na in
+      if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+      else na in
     let impl = match na with
-     | Name id -> Some (ExplByName id,Manual,(true,true))
-     | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
-     impl :: acc
+      | Name id -> Some (ExplByName id,Manual,(max,true))
+      | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in
+    impl
+  in
+  match bk with
+  | NonMaxImplicit -> impl_status false :: acc
+  | MaxImplicit -> impl_status true :: acc
   | Explicit -> None :: acc
 
 let impls_binder_list =
@@ -426,7 +429,7 @@ let warn_unexpected_implicit_binder_declaration =
     Pp.(fun () -> str "Unexpected implicit binder declaration.")
 
 let check_implicit_meaningful ?loc k env =
-  if k = Implicit && env.impl_binder_index = None then
+  if k <> Explicit && env.impl_binder_index = None then
     warn_unexpected_implicit_binder_declaration ?loc ()
 
 let intern_generalized_binder intern_type ntnvars
@@ -444,7 +447,7 @@ let intern_generalized_binder intern_type ntnvars
   check_implicit_meaningful ?loc b' env;
   let bl = List.map
     CAst.(map (fun id ->
-      (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+      (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -2500,8 +2503,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
               let r = Retyping.relevance_of_type env sigma t in
               let d = LocalAssum (make_annot na r,t) in
               let impls =
-                if k == Implicit then CAst.make (Some (na,true)) :: impls
-                else CAst.make None :: impls
+                match k with
+                | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls
+                | MaxImplicit -> CAst.make (Some (na,true)) :: impls
+                | Explicit -> CAst.make None :: impls
               in
                 (push_rel d env, sigma, d::params, succ n, impls)
           | Some b ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e2c732809a..9b50d9ca71 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Constr
 open Globnames
+open Glob_term
 open Declarations
 open Lib
 open Libobject
@@ -80,10 +81,24 @@ let with_implicit_protection f x =
     let () = implicit_args := oflags in
     iraise reraise
 
-let set_maximality imps b =
+type on_trailing_implicit = Error | Info | Silent
+
+let msg_trailing_implicit (fail : on_trailing_implicit) id =
+  let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in
+  match fail with
+  | Error ->
+    user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ]."))
+  | Info ->
+    Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted."))
+  | Silent -> ()
+
+let set_maximality fail id imps b =
   (* Force maximal insertion on ending implicits (compatibility) *)
-  let is_set x = match x with None -> false | _ -> true in
-  b || List.for_all is_set imps
+  b || (
+    let is_set x = match x with None -> false | _ -> true in
+    let b' = List.for_all is_set imps in
+    if b' then msg_trailing_implicit fail id;
+    b')
 
 (*s Computation of implicit arguments *)
 
@@ -302,6 +317,11 @@ let is_status_implicit = function
 
 let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
 
+let binding_kind_of_status = function
+  | Some (_, _, (false, _)) -> NonMaxImplicit
+  | Some (_, _, (true, _)) -> MaxImplicit
+  | None -> Explicit
+
 let name_of_implicit = function
   | None -> anomaly (Pp.str "Not an implicit argument.")
   | Some (ExplByName id,_,_) -> id
@@ -340,19 +360,19 @@ let rec prepare_implicits f = function
   | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
   | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
-      Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+      Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-let set_manual_implicits flags enriching autoimps l =
+let set_manual_implicits silent flags enriching autoimps l =
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k autoimps explimps = match autoimps, explimps with
     | autoimp::autoimps, explimp::explimps ->
        let imps' = merge (k+1) autoimps explimps in
        begin match autoimp, explimp.CAst.v with
        | (Name id,_), Some (_,max) ->
-          Some (ExplByName id, Manual, (set_maximality imps' max, true))
+          Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true))
        | (Name id,Some exp), None when enriching ->
-          Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
+          Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true))
        | (Name _,_), None -> None
        | (Anonymous,_), Some (Name id,max) ->
           Some (ExplByName id,Manual,(max,true))
@@ -497,8 +517,9 @@ let impls_of_context ctx =
   let map decl =
     let id = NamedDecl.get_id decl in
     match Id.Map.get id !sec_implicits with
-    | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
-    | Glob_term.Explicit -> None
+    | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true))
+    | MaxImplicit -> Some (ExplByName id, Manual, (true, true))
+    | Explicit -> None
   in
   List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
 
@@ -608,7 +629,7 @@ type manual_implicits = (Name.t * bool) option CAst.t list
 
 let compute_implicits_with_manual env sigma typ enriching l =
   let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
-  set_manual_implicits !implicit_args enriching autoimpls l
+  set_manual_implicits true !implicit_args enriching autoimpls l
 
 let check_inclusion l =
   (* Check strict inclusion *)
@@ -636,7 +657,7 @@ 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 l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in
   let req =
     if is_local local ref then ImplLocal
     else ImplInteractive(flags,ImplManual (List.length autoimpls))
@@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l =
     declare_manual_implicits local ref ?enriching l
 
 
-let msg_trailing_implicit id =
-  user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]."))
-
-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 ->
+    | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+    | Name id :: autoimps, MaxImplicit :: manualimps ->
        Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
-    | Name id :: autoimps, Implicit :: manualimps ->
+    | Name id :: autoimps, NonMaxImplicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
-       let max = set_maximality imps' false in
-       if max then msg_trailing_implicit id;
+       let max = set_maximality Error id imps' false in
        Some (ExplByName id, Manual, (max, true)) :: imps'
-    | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
+    | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ ->
        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
@@ -684,7 +699,7 @@ let set_implicits local ref l =
        check_rigidity (is_rigid env sigma t);
        (* Sort by number of implicits, decreasing *)
        let is_implicit = function
-         | NotImplicit -> false
+         | Explicit -> 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
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ef3c2496f4..65e7fd8aaf 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -77,6 +77,7 @@ type implicit_side_condition
 type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
+val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> Id.t
 val maximal_insertion_of : implicit_status -> bool
@@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
 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 set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
 
 val implicits_of_global : GlobRef.t -> implicits_list list
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8b457ab37b..ffbb982ab7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -203,8 +203,9 @@ let warn_ignoring_implicit_status =
 
 let implicits_of_glob_constr ?(with_products=true) l =
   let add_impl ?loc na bk l = match bk with
-  | Implicit -> CAst.make ?loc (Some (na,true)) :: l
-  | _ -> CAst.make ?loc None :: l
+  | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l
+  | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l
+  | Explicit -> CAst.make ?loc None :: l
   in
   let rec aux c =
     match DAst.get c with
@@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
       if with_products then add_impl na bk (aux b)
       else
         let () = match bk with
-          | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
-          | _ -> ()
+          | NonMaxImplicit
+          | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
+          | Explicit -> ()
         in []
     | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
     | GLetIn (na, b, t, c) -> aux c
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index af1e973261..dcc3a87b11 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram
       | "{"; c = binder_constr ; "}" ->
         { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
-        { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
+        { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
@@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram
       | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
         { [CLocalDef (id,c,Some t)] }
       | "{"; id = name; "}" ->
-        { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+        { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
       | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum (id::idl,Default Implicit,c)] }
+        { [CLocalAssum (id::idl,Default MaxImplicit,c)] }
       | "{"; id = name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum ([id],Default Implicit,c)] }
+        { [CLocalAssum ([id],Default MaxImplicit,c)] }
       | "{"; id = name; idl = LIST1 name; "}" ->
-        { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+        { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+      | "["; id = name; "]" ->
+        { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+      | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" ->
+        { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] }
+      | "["; id = name; ":"; c = lconstr; "]" ->
+        { [CLocalAssum ([id],Default NonMaxImplicit,c)] }
+      | "["; id = name; idl = LIST1 name; "]" ->
+        { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc }
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
+      | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
       | "'"; p = pattern LEVEL "0" ->
         { let (p, ty) =
             match p.CAst.v with
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d8dbf2f3dc..b212e7046a 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -151,7 +151,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 ->
-    Impargs.MaximallyImplicit :: loop args'
+    MaxImplicit :: loop args'
   | args' when List.exists Impargs.is_status_implicit args' ->
       errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
   | _ -> [] in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 02c2fc4a13..0969b3cc03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true
-  | Implicit, Implicit -> true
-  | (Explicit | Implicit), _ -> false
+  | NonMaxImplicit, NonMaxImplicit -> true
+  | MaxImplicit, MaxImplicit -> true
+  | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
 
 let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 44323441b6..485a19421d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
 
 type cases_pattern = [ `any ] cases_pattern_g
 
-type binding_kind = Explicit | Implicit
+type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
 
 (** Representation of an internalized (or in other words globalized) term. *)
 type 'a glob_constr_r =
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index b55a41471a..2416819a6a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -143,7 +143,8 @@ let tag_var = tag Tag.variable
   let pr_generalization bk ak c =
     let hd, tl =
       match bk with
-        | Implicit -> "{", "}"
+        | NonMaxImplicit -> "[", "]"
+        | MaxImplicit -> "{", "}"
         | Explicit -> "(", ")"
     in (* TODO: syntax Abstraction Kind *)
     str "`" ++ str hd ++ c ++ str tl
@@ -324,12 +325,14 @@ let tag_var = tag Tag.variable
   let surround_impl k p =
     match k with
       | Explicit -> str"(" ++ p ++ str")"
-      | Implicit -> str"{" ++ p ++ str"}"
+      | NonMaxImplicit -> str"[" ++ p ++ str"]"
+      | MaxImplicit -> str"{" ++ p ++ str"}"
 
   let surround_implicit k p =
     match k with
       | Explicit -> p
-      | Implicit -> (str"{" ++ p ++ str"}")
+      | NonMaxImplicit -> str"[" ++ p ++ str"]"
+      | MaxImplicit -> (str"{" ++ p ++ str"}")
 
   let pr_binder many pr (nal,k,t) =
     match k with
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index de34e007d2..df729588f4 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -11,4 +11,10 @@ Admitted.
 Print a_eq_b.
 
 
+Require Import Morphisms.
 
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True.
+Admitted.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index b16e4a1186..e68040e4d4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -1,3 +1,15 @@
+
+Axiom foo : forall (x y z t : nat), nat.
+
+Arguments foo {_} _ [z] t.
+Check (foo 1).
+Arguments foo {_} _ {z} {t}.
+Fail Arguments foo {_} _ [z] {t}.
+Check (foo 1).
+
+Definition foo1 [m] n := n + m.
+Check (foo1 1).
+
 Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
@@ -33,3 +45,11 @@ Abort.
 
 Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
 Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
+
+Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'.
+Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b.
+Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b.
+
+Definition F (id: forall [A] [x : A], A) := id.
+Definition G := let id := (fun [A] (x : A) => x) in id.
+Fail Definition G' := let id := (fun {A} (x : A) => x) in id.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ecaaedca53..668d765d83 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -114,9 +114,13 @@ Check h 0.
 Inductive I {A} (a:A) : forall {n:nat}, Prop :=
  | C : I a (n:=0).
 
+Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop :=
+ | C' : I' a eq_refl.
+
 Inductive I2 (x:=0) : Prop :=
- | C2 {p:nat} : p = 0 -> I2.
-Check C2 eq_refl.
+ | C2 {p:nat} : p = 0 -> I2
+ | C2' [p:nat] : p = 0 -> I2.
+Check C2' eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
@@ -147,6 +151,7 @@ Set Warnings "syntax".
 (* Miscellaneous tests *)
 
 Check let f := fun {x:nat} y => y=true in f false.
+Check let f := fun [x:nat] y => y=true in f false.
 
 (* Isn't the name "arg_1" a bit fragile, here? *)
 
@@ -157,3 +162,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0).
 Set Warnings "+syntax".
 Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
 Set Warnings "syntax".
+
+
+Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0.
+Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0.
+Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0.
+Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted.
+Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 77bc4e4f8a..b92c9e9b71 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
 let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass =
-    if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
+    if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
     else tclass
   in
   let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 15077298aa..9d43debb77 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags =
 
   let implicits = List.map (List.map snd) implicits in
   let implicits_specified = match implicits with
-    | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+    | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
     | _ -> true in
 
   if implicits_specified && clear_implicits_flag then
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index 71effddf67..cbc5fc15e2 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -12,6 +12,6 @@ val vernac_arguments
   : section_local:bool
   -> Libnames.qualid Constrexpr.or_by_notation
   -> Vernacexpr.vernac_argument_status list
-  -> (Names.Name.t * Impargs.implicit_kind) list list
+  -> (Names.Name.t * Glob_term.binding_kind) list list
   -> Vernacexpr.arguments_modifier list
   -> unit
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 625ffb5a06..d97bf6724c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -270,7 +270,7 @@ let context ~poly l =
         | Some (Name id',_) -> Id.equal name id'
         | _ -> false
       in
-      let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in
+      let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
       name,b,t,impl)
       ctx
   in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3302231fd1..d0374bc4fa 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,7 +16,6 @@ open Util
 open Names
 open Glob_term
 open Vernacexpr
-open Impargs
 open Constrexpr
 open Constrexpr_ops
 open Extend
@@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram
       { let name, recarg_like, notation_scope = item in
       [RealArg { name=name; recarg_like=recarg_like;
              notation_scope=notation_scope;
-             implicit_status = NotImplicit}] }
+             implicit_status = Explicit}] }
     | "/" -> { [VolatileArg] }
     | "&" -> { [BidiArg] }
     | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
@@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram
        List.map (fun (name,recarg_like,notation_scope) ->
            RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
-                 implicit_status = NotImplicit}) items }
+                 implicit_status = Explicit}) items }
     | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram
        List.map (fun (name,recarg_like,notation_scope) ->
            RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
-                 implicit_status = Implicit}) items }
+                 implicit_status = NonMaxImplicit}) items }
     | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram
        List.map (fun (name,recarg_like,notation_scope) ->
            RealArg { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
-                 implicit_status = MaximallyImplicit}) items }
+                 implicit_status = MaxImplicit}) items }
     ]
   ];
   (* Same as [argument_spec_block], but with only implicit status and names *)
   more_implicits_block: [
-    [ name = name -> { [(name.CAst.v, NotImplicit)] }
+    [ name = name -> { [(name.CAst.v, Explicit)] }
     | "["; items = LIST1 name; "]" ->
-       { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
+       { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
     | "{"; items = LIST1 name; "}" ->
-       { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
+       { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
     ]
   ];
   strategy_level:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a1bd99c237..82132a1af6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function
               let pr_br imp force x =
                 let left,right =
                 match imp with
-                | Impargs.Implicit -> str "[", str "]"
-                | Impargs.MaximallyImplicit -> str "{", str "}"
-                | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+                | Glob_term.NonMaxImplicit -> str "[", str "]"
+                | Glob_term.MaxImplicit -> str "{", str "}"
+                | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
                 in
                 left ++ x ++ right
               in
               let get_arguments_like s imp tl =
-                if s = None && imp = Impargs.NotImplicit then [], tl
+                if s = None && imp = Glob_term.Explicit then [], tl
                 else
                   let rec fold extra = function
                     | RealArg arg :: tl when
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2cd1cf7c65..62ba6b157a 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -260,18 +260,18 @@ let implicit_name_of_pos = function
   | Constrexpr.ExplByPos (n,k) -> Anonymous
 
 let implicit_kind_of_status = function
-  | None -> Anonymous, NotImplicit
-  | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
+  | None -> Anonymous, Glob_term.Explicit
+  | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
 
 let dummy = {
-  Vernacexpr.implicit_status = NotImplicit;
+  Vernacexpr.implicit_status = Glob_term.Explicit;
   name = Anonymous;
   recarg_like = false;
   notation_scope = None;
 }
 
 let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
-  name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
+  name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
 
 let rec main_implicits i renames recargs scopes impls =
   if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -283,8 +283,8 @@ let rec main_implicits i renames recargs scopes impls =
     let (name, implicit_status) =
       match renames, impls with
       | _, (Some _ as i) :: _ -> implicit_kind_of_status i
-      | name::_, _ -> (name,NotImplicit)
-      | [], (None::_ | []) -> (Anonymous, NotImplicit)
+      | name::_, _ -> (name,Glob_term.Explicit)
+      | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
     in
     let notation_scope = match scopes with
       | scope :: _ -> Option.map CAst.make scope
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 1daa244986..22a8de7f99 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -254,7 +254,7 @@ type vernac_one_argument_status = {
   name : Name.t;
   recarg_like : bool;
   notation_scope : string CAst.t option;
-  implicit_status : Impargs.implicit_kind;
+  implicit_status : Glob_term.binding_kind;
 }
 
 type vernac_argument_status =
@@ -386,7 +386,7 @@ type nonrec vernac_expr =
   | VernacArguments of
       qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
-      (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
+      (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) *
       arguments_modifier list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option