Pass unnamed arguments to ML macros.

This was imposing a bit of useless burden on the API for no good reason.

12 files changed, 49 insertions, 75 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d9fff46d88..42d8528a8c 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -296,17 +296,16 @@ let rec print_symbol fmt = function
 let rec print_clause fmt = function
 | [] -> fprintf fmt "@[TyNil@]"
 | ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl
-| ExtNonTerminal (g, TokNone) :: cl ->
-  fprintf fmt "@[TyAnonArg (%a, %a)@]"
+| ExtNonTerminal (g, _) :: cl ->
+  fprintf fmt "@[TyArg (%a, %a)@]"
     print_symbol g print_clause cl
-| ExtNonTerminal (g, TokName id) :: cl ->
-  fprintf fmt "@[TyArg (%a, \"%s\", %a)@]"
-    print_symbol g id print_clause cl
 
 let rec print_binders fmt = function
 | [] -> fprintf fmt "ist@ "
-| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem
-| (ExtNonTerminal (_, TokName id)) :: rem ->
+| ExtTerminal _ :: rem -> print_binders fmt rem
+| ExtNonTerminal (_, TokNone) :: rem ->
+  fprintf fmt "_@ %a" print_binders rem
+| ExtNonTerminal (_, TokName id) :: rem ->
   fprintf fmt "%s@ %a" id print_binders rem
 
 let print_rule fmt r =
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e15fd776b2..4c089eeb01 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -527,7 +527,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -543,7 +543,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index f3af318b60..b163100fc3 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -50,3 +50,5 @@ val type_of_user_symbol : user_symbol -> argument_type
 val parse_user_entry : string -> string -> user_symbol
 
 val mlexpr_of_symbol : user_symbol -> MLast.expr
+
+val binders_of_tokens : MLast.expr -> extend_token list -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0e2bf55d86..a2007d258c 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -142,3 +142,9 @@ let rec mlexpr_of_symbol = function
   assert (e = "tactic");
   let wit = <:expr< $lid:"wit_"^e$ >> in
   <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
+
+let rec binders_of_tokens e = function
+| [] -> e
+| ExtNonTerminal(_,None) :: cl -> <:expr< fun _ -> $binders_of_tokens e cl$ >>
+| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_tokens e cl$ >>
+| ExtTerminal _ :: cl -> binders_of_tokens e cl
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 5943600b7c..a093f78388 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -20,16 +20,8 @@ let plugin_name = <:expr< __coq_plugin_name >>
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
-| ExtNonTerminal(g,None) :: cl ->
-  <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
-| ExtNonTerminal(g,Some id) :: cl ->
-  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >>
-
-let rec binders_of_clause e = function
-| [] -> <:expr< fun ist -> $e$ >>
-| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
-| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
-| _ :: cl -> binders_of_clause e cl
+| ExtNonTerminal (g, _) :: cl ->
+  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 open Pcaml
 
@@ -52,7 +44,8 @@ EXTEND
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
         "->"; "["; e = Pcaml.expr; "]" ->
-         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
+        let e = <:expr< fun ist -> $e$ >> in
+         <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >>
     ] ]
   ;
 
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f30c96a7f5..3c401e827e 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -24,23 +24,16 @@ type rule = {
   (** Whether this entry is deprecated *)
 }
 
-let rec make_patt r = function
-| [] -> r
-| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
-| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
-| ExtTerminal _ :: l -> make_patt r l
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< Vernacentries.TyNil >>
 | ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
 | ExtNonTerminal (g, id) :: cl ->
-  let id = mlexpr_of_option mlexpr_of_string id in
-  <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
+  <:expr< Vernacentries.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 let make_rule r =
   let ty = mlexpr_of_clause r.r_patt in
-  let cmd = make_patt r.r_branch r.r_patt in
-  let make_classifier c = make_patt c r.r_patt in
+  let cmd = binders_of_tokens r.r_branch r.r_patt in
+  let make_classifier c = binders_of_tokens c r.r_patt in
   let classif = mlexpr_of_option make_classifier r.r_class in
   <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 636cb8ebf8..a77a9c2f45 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -187,7 +187,7 @@ let add_tactic_entry (kn, ml, tg) state =
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, (s, ido)) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
+    GramNonTerminal (Loc.tag ?loc @@ (typ, e))
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -556,18 +556,14 @@ let () =
   ] in
   register_grammars_by_name "tactic" entries
 
-let get_identifier id =
+let get_identifier i =
   (** Workaround for badly-designed generic arguments lacking a closure *)
-  Names.Id.of_string_soft ("$" ^ id)
-
+  Names.Id.of_string_soft (Printf.sprintf "$%i" i)
 
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
-| TyArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
-| TyAnonArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
+| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
@@ -581,18 +577,16 @@ let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.a
   | TUentry a -> Uentry (Genarg.ArgT.Any a)
   | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
 
-let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
-  fun sign -> match sign with
+let rec clause_of_sign : type a. int -> a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+  fun i sign -> match sign with
   | TyNil -> []
-  | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
-  | TyArg (a, id, sig') ->
-    let id = get_identifier id in
-    TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
-  | TyAnonArg (a, sig') ->
-    TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig'
+  | TyIdent (s, sig') -> TacTerm s :: clause_of_sign i sig'
+  | TyArg (a, sig') ->
+    let id = Some (get_identifier i) in
+    TacNonTerm (None, (untype_user_symbol a, id)) :: clause_of_sign (i + 1) sig'
 
 let clause_of_ty_ml = function
-  | TyML (t,_) -> clause_of_sign t
+  | TyML (t,_) -> clause_of_sign 1 t
 
 let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
   fun sign tac ->
@@ -603,7 +597,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
       | _ :: _ -> assert false
       end
     | TyIdent (s, sig') -> eval_sign sig' tac
-    | TyArg (a, _, sig') ->
+    | TyArg (a, sig') ->
       let f = eval_sign sig' in
       begin fun tac vals ist -> match vals with
       | [] -> assert false
@@ -611,7 +605,6 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
         let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
         f (tac v') vals ist
       end tac
-    | TyAnonArg (a, sig') -> eval_sign sig' tac
 
 let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
   | TyML (t,tac) -> eval_sign t tac
@@ -623,14 +616,12 @@ let is_constr_entry = function
 let rec only_constr : type a. a ty_sig -> bool = function
 | TyNil -> true
 | TyIdent(_,_) -> false
-| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false
-| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false
+| TyArg (u, s) -> if is_constr_entry u then only_constr s else false
 
-let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+let rec mk_sign_vars : type a. int -> a ty_sig -> Name.t list = fun i tu -> match tu with
 | TyNil -> []
-| TyIdent (_,s) -> mk_sign_vars s
-| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s
-| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s
+| TyIdent (_,s) -> mk_sign_vars i s
+| TyArg (_, s) -> Name (get_identifier i) :: mk_sign_vars (i + 1) s
 
 let dummy_id = Id.of_string "_"
 
@@ -661,12 +652,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
   (** The extension is only made of a name followed by constr entries: we do not
       add any grammar nor printing rule and add it as a true Ltac definition. *)
-    (*
-    let patt = make_patt rem in
-    let vars = List.map make_var rem in
-    let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
-       *)
-    let vars = mk_sign_vars s in
+    let vars = mk_sign_vars 1 s in
     let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
     let tac = match s with
     | TyNil -> eval ml_tac
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 138a584e01..0b2b426018 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -73,10 +73,7 @@ val print_located_tactic : Libnames.qualid -> unit
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
-| TyArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
-| TyAnonArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
+| TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index c5dedc880e..89caff847f 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,7 +19,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+      ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -40,7 +40,7 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
+  let inj = Some (fun obj -> Genarg.in_gen t obj) in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index c4f4fcfaa4..a90ef97e7d 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -17,7 +17,7 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
+  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 015d5fabef..80312d94fa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2497,8 +2497,7 @@ type classifier = Genarg.raw_generic_argument list -> vernac_classification
 type (_, _) ty_sig =
 | TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
-| TyNonTerminal :
-  string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
 type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
 
@@ -2511,7 +2510,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio
   | _ :: _ -> type_error ()
   end
 | TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
   begin match args with
   | [] -> type_error ()
   | Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2528,7 +2527,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm
   | _ :: _ -> type_error ()
   end
 | TyTerminal (_, ty) -> fun f args -> untype_command ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
   begin match args with
   | [] -> type_error ()
   | Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2549,8 +2548,8 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s
 let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
 | TyNil -> []
 | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
-| TyNonTerminal (id, tu, ty) ->
-  let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+| TyNonTerminal (tu, ty) ->
+  let t = rawwit (Egramml.proj_symbol tu) in
   let symb = untype_user_symbol tu in
   Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index fb2a30bac7..34f6029e78 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,7 +51,6 @@ type (_, _) ty_sig =
 | TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
-  string option *
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
     ('a -> 'r, 'a -> 's) ty_sig