Removing the default value mechanism for generic arguments.

There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.

2 files changed, 4 insertions, 18 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index c7273ac93e..7aada461f5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -246,7 +246,6 @@ struct
 end
 
 type ('raw, 'glb, 'top) load = {
-  nil : 'raw option;
   dyn : 'top Val.tag;
 }
 
@@ -254,30 +253,19 @@ module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
 
 let arg0_map = ref LoadMap.empty
 
-let create_arg opt ?dyn name =
+let create_arg ?dyn name =
   match ArgT.name name with
   | Some _ ->
     Errors.anomaly (str "generic argument already declared: " ++ str name)
   | None ->
     let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
-    let obj = LoadMap.Pack { nil = opt; dyn; } in
+    let obj = LoadMap.Pack { dyn; } in
     let name = ArgT.create name in
     let () = arg0_map := LoadMap.add name obj !arg0_map in
     ExtraArg name
 
 let make0 = create_arg
 
-let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function
-| ListArg _ -> Some []
-| OptArg _ -> Some None
-| PairArg (t1, t2) ->
-  begin match default_empty_value t1, default_empty_value t2 with
-  | Some v1, Some v2 -> Some (v1, v2)
-  | _ -> None
-  end
-| ExtraArg s ->
-  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil
-
 let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
 | ListArg t -> Val.List (val_tag t)
 | OptArg t -> Val.Opt (val_tag t)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index ce0536cf49..d509649f22 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -110,11 +110,11 @@ end
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -250,8 +250,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
 
 (** {5 Magic used by the parser} *)
 
-val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-
 val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
 (** Used by the extension to give a name to types. The string should be the
     absolute path of the argument witness, e.g.