Merge PR #8161: Implement VERNAC EXTEND in coqpp

17 files changed, 240 insertions, 120 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 956a916792..6f697f5d49 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -85,12 +85,31 @@ type tactic_ext = {
   tacext_rules : tactic_rule list;
 }
 
+type classification =
+| ClassifDefault
+| ClassifCode of code
+| ClassifName of string
+
+type vernac_rule = {
+  vernac_toks : ext_token list;
+  vernac_class : code option;
+  vernac_depr : bool;
+  vernac_body : code;
+}
+
+type vernac_ext = {
+  vernacext_name : string;
+  vernacext_entry : code option;
+  vernacext_class : classification;
+  vernacext_rules : vernac_rule list;
+}
+
 type node =
 | Code of code
 | Comment of string
 | DeclarePlugin of string
 | GramExt of grammar_ext
-| VernacExt
+| VernacExt of vernac_ext
 | TacticExt of tactic_ext
 
 type t = node list
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 81a53e887b..d809b824df 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -95,12 +95,16 @@ rule extend = parse
 | "{" { start_ocaml lexbuf; ocaml lexbuf }
 | "GRAMMAR" { GRAMMAR }
 | "VERNAC" { VERNAC }
+| "COMMAND" { COMMAND }
 | "TACTIC" { TACTIC }
 | "EXTEND" { EXTEND }
 | "END" { END }
 | "DECLARE" { DECLARE }
 | "PLUGIN" { PLUGIN }
 | "DEPRECATED" { DEPRECATED }
+| "CLASSIFIED" { CLASSIFIED }
+| "BY" { BY }
+| "AS" { AS }
 (** Camlp5 specific keywords *)
 | "GLOBAL" { GLOBAL }
 | "FIRST" { FIRST }
@@ -122,6 +126,7 @@ rule extend = parse
 | ']' { RBRACKET }
 | '|' { PIPE }
 | "->" { ARROW }
+| "=>" { FUN }
 | ',' { COMMA }
 | ':' { COLON }
 | ';' { SEMICOLON }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index d9fff46d88..89b4d340b2 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -64,6 +64,39 @@ let string_split s =
 
 let plugin_name = "__coq_plugin_name"
 
+let print_list fmt pr l =
+  let rec prl fmt = function
+  | [] -> ()
+  | [x] -> fprintf fmt "%a" pr x
+  | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
+  in
+  fprintf fmt "@[<hv>[%a]@]" prl l
+
+let rec print_binders fmt = function
+| [] -> ()
+| 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 rec print_symbol fmt = function
+| Ulist1 s ->
+  fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
+| Ulist1sep (s, sep) ->
+  fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
+| Ulist0 s ->
+  fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
+| Ulist0sep (s, sep) ->
+  fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
+| Uopt s ->
+  fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
+| Uentry e ->
+  fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
+
 module GramExt :
 sig
 
@@ -104,14 +137,6 @@ let print_local fmt ext =
 
 let print_string fmt s = fprintf fmt "\"%s\"" s
 
-let print_list fmt pr l =
-  let rec prl fmt = function
-  | [] -> ()
-  | [x] -> fprintf fmt "%a" pr x
-  | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
-  in
-  fprintf fmt "@[<hv>[%a]@]" prl l
-
 let print_opt fmt pr = function
 | None -> fprintf fmt "None"
 | Some x -> fprintf fmt "Some@ (%a)" pr x
@@ -268,6 +293,61 @@ let print_ast fmt ext =
 
 end
 
+module VernacExt :
+sig
+
+val print_ast : Format.formatter -> vernac_ext -> unit
+
+end =
+struct
+
+let print_rule_classifier fmt r = match r.vernac_class with
+| None -> fprintf fmt "None"
+| Some f -> fprintf fmt "Some @[(fun %a-> %s)@]" print_binders r.vernac_toks f.code
+
+let print_body fmt r =
+  fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %s in st)@]"
+    print_binders r.vernac_toks r.vernac_body.code
+
+let rec print_sig fmt = function
+| [] -> fprintf fmt "@[Vernacentries.TyNil@]"
+| ExtTerminal s :: rem ->
+  fprintf fmt "@[Vernacentries.TyTerminal (\"%s\", %a)@]" s print_sig rem
+| ExtNonTerminal (symb, _) :: rem ->
+  fprintf fmt "@[Vernacentries.TyNonTerminal (%a, %a)@]"
+    print_symbol symb print_sig rem
+
+let print_rule fmt r =
+  fprintf fmt "Vernacentries.TyML (%b, %a, %a, %a)"
+    r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r
+
+let print_rules fmt rules =
+  print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
+
+let print_classifier fmt = function
+| ClassifDefault -> fprintf fmt ""
+| ClassifName "QUERY" ->
+  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)"
+| ClassifName "SIDEFF" ->
+  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)"
+| ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
+| ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
+
+let print_entry fmt = function
+| None -> fprintf fmt "None"
+| Some e -> fprintf fmt "Some (%s)" e.code
+
+let print_ast fmt ext =
+  let pr fmt () =
+    fprintf fmt "Vernacentries.vernac_extend ~command:\"%s\" %a ?entry:%a %a"
+      ext.vernacext_name print_classifier ext.vernacext_class
+      print_entry ext.vernacext_entry print_rules ext.vernacext_rules
+  in
+  let () = fprintf fmt "let () = @[%a@]@\n" pr () in
+  ()
+
+end
+
 module TacticExt :
 sig
 
@@ -276,50 +356,19 @@ val print_ast : Format.formatter -> tactic_ext -> unit
 end =
 struct
 
-let rec print_symbol fmt = function
-| Ulist1 s ->
-  fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
-| Ulist1sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
-| Ulist0 s ->
-  fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
-| Ulist0sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
-| Uopt s ->
-  fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
-| Uentry e ->
-  fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
-
 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)@]"
+| [] -> fprintf fmt "@[Tacentries.TyNil@]"
+| ExtTerminal s :: cl -> fprintf fmt "@[Tacentries.TyIdent (\"%s\", %a)@]" s print_clause cl
+| ExtNonTerminal (g, _) :: cl ->
+  fprintf fmt "@[Tacentries.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 ->
-  fprintf fmt "%s@ %a" id print_binders rem
 
 let print_rule fmt r =
-  fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]"
+  fprintf fmt "@[Tacentries.TyML (%a, @[fun %aist@ -> %a@])@]"
     print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body
 
-let rec print_rules fmt = function
-| [] -> ()
-| [r] -> fprintf fmt "(%a)@\n" print_rule r
-| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem
-
 let print_rules fmt rules =
-  fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
+  print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
 
 let print_ast fmt ext =
   let deprecation fmt =
@@ -348,7 +397,7 @@ let pr_ast fmt = function
 | Comment s -> fprintf fmt "%s@\n" s
 | DeclarePlugin name -> declare_plugin fmt name
 | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
-| VernacExt -> fprintf fmt "VERNACEXT@\n"
+| VernacExt vernac -> fprintf fmt "%a@\n" VernacExt.print_ast vernac
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
 
 let () =
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index bf435fd247..31f234c37f 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -63,7 +63,8 @@ let parse_user_entry s sep =
 %token <string> STRING
 %token <int> INT
 %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED
-%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
+%token COMMAND CLASSIFIED BY AS
+%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
 %token EOF
@@ -104,7 +105,49 @@ grammar_extend:
 ;
 
 vernac_extend:
-| VERNAC EXTEND IDENT END { VernacExt }
+| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END
+  { VernacExt {
+    vernacext_name = $4;
+    vernacext_entry = $2;
+    vernacext_class = $5;
+    vernacext_rules = $6;
+  } }
+;
+
+vernac_entry:
+| COMMAND { None }
+| CODE { Some $1 }
+;
+
+vernac_classifier:
+| { ClassifDefault }
+| CLASSIFIED BY CODE { ClassifCode $3 }
+| CLASSIFIED AS IDENT { ClassifName $3 }
+;
+
+vernac_rules:
+| vernac_rule { [$1] }
+| vernac_rule vernac_rules { $1 :: $2 }
+;
+
+vernac_rule:
+| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+  { {
+      vernac_toks = $3;
+      vernac_depr = $5;
+      vernac_class= $6;
+      vernac_body = $8;
+  } }
+;
+
+rule_deprecation:
+| { false }
+| DEPRECATED { true }
+;
+
+rule_classifier:
+| { None }
+| FUN CODE { Some $2 }
 ;
 
 tactic_extend:
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7e64f80ac5..40013712fd 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -176,7 +176,28 @@ END
 
 #### VERNAC EXTEND
 
-Not handled yet.
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions and rule classifiers with
+  braces
+- if not there yet, add a leading `|̀  to the first rule
+
+Handwritten classifiers declared through the `CLASSIFIED BY` statement are
+considered OCaml code, so they also need to be wrapped in braces.
+
+For instance, code of the form:
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier
+  [ "foo" int(i) ] => [ classif' ] -> [ cmd1 i ]
+| [ "bar" ] -> [ cmd2 ]
+END
+```
+should be turned into
+```
+VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier }
+| [ "foo" int(i) ] => { classif' } -> { cmd1 i }
+| [ "bar" ] -> { cmd2 }
+END
+```
 
 #### ARGUMENT EXTEND
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8129a4a867..44d44ccc4b 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/derive/g_derive.ml4 b/plugins/derive/g_derive.mlg
index a59324149c..18316bf2cd 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.mlg
@@ -8,13 +8,21 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Stdarg
 
+}
+
 DECLARE PLUGIN "derive_plugin"
 
+{
+
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
-VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
+}
+
+VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
 | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-     [ Derive.start_deriving f suchthat lemma ]
+  { Derive.start_deriving f suchthat lemma }
 END
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 cf2fecb9c1..378100ac69 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2496,8 +2496,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
 
@@ -2510,7 +2509,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 ->
@@ -2527,7 +2526,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 ->
@@ -2548,8 +2547,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