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, 8 insertions, 32 deletions

diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index d620febbc1..32ccf21d2b 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -32,7 +32,7 @@ let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Spec
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
 let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
-  Genarg.create_arg None "withtac"
+  Genarg.create_arg "withtac"
 
 let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 98d1a23770..82bd5dac4c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -158,36 +158,10 @@ type ml_tactic_grammar_obj = {
 
 exception NonEmptyArgument
 
-let default_empty_value wit = match Genarg.default_empty_value wit with
-| None -> raise NonEmptyArgument
-| Some v -> v
-
-let rec empty_value : type a b c s. (a, b, c) Genarg.genarg_type -> (s, a) entry_key -> a =
-fun wit key -> match key with
-| Alist1 key ->
-  begin match wit with
-  | Genarg.ListArg wit -> [empty_value wit key]
-  | Genarg.ExtraArg _ -> default_empty_value wit
-  end
-| Alist1sep (key, _) ->
-  begin match wit with
-  | Genarg.ListArg wit -> [empty_value wit key]
-  | Genarg.ExtraArg _ -> default_empty_value wit
-  end
-| Alist0 _ -> []
-| Alist0sep (_, _) -> []
-| Amodifiers _ -> []
-| Aopt _ -> None
-| Aentry _ -> default_empty_value wit
-| Aentryl (_, _) -> default_empty_value wit
-
-| Atoken _ -> raise NonEmptyArgument
-| Aself -> raise NonEmptyArgument
-| Anext -> raise NonEmptyArgument
-
 (** ML tactic notations whose use can be restricted to an identifier are added
     as true Ltac entries. *)
 let extend_atomic_tactic name entries =
+  let open Tacexpr in
   let map_prod prods =
     let (hd, rem) = match prods with
     | GramTerminal s :: rem -> (s, rem)
@@ -197,8 +171,11 @@ let extend_atomic_tactic name entries =
     | GramTerminal s -> raise NonEmptyArgument
     | GramNonTerminal (_, typ, e) ->
       let Genarg.Rawwit wit = typ in
-      let def = Genarg.in_gen typ (empty_value wit e) in
-      Tacintern.intern_genarg Tacintern.fully_empty_glob_sign def
+      let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
+      let default = epsilon_value inj e in
+      match default with
+      | None -> raise NonEmptyArgument
+      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
     in
     try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
   in
@@ -206,8 +183,7 @@ let extend_atomic_tactic name entries =
   let add_atomic i args = match args with
   | None -> ()
   | Some (id, args) ->
-    let open Tacexpr in
-    let args = List.map (fun a -> TacGeneric a) args in
+    let args = List.map (fun a -> Tacexp a) args in
     let entry = { mltac_name = name; mltac_index = i } in
     let body = TacML (Loc.ghost, entry, args) in
     Tacenv.register_ltac false false (Names.Id.of_string id) body