Add syntax for non maximally inserted implicit arguments

8 files changed, 23 insertions, 24 deletions

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