From 270ceed48217797e99ec845cc5d1c599b5729bc2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Jul 2018 15:11:05 +0200
Subject: Export a wrapper simplifying the registration of vernacular commands.

---
 grammar/vernacextend.mlp  | 80 +++++++++++++----------------------------------
 stm/vernac_classifier.ml  |  9 +-----
 stm/vernac_classifier.mli |  5 ---
 vernac/vernacentries.ml   | 49 +++++++++++++++++++++++++++++
 vernac/vernacentries.mli  | 23 ++++++++++++++
 5 files changed, 95 insertions(+), 71 deletions(-)

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index a2872d07f6..f344f3c573 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -66,54 +66,13 @@ let mk_ignore c pt =
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
 
-let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
-  match c ,cg with
-  | Some c, _ ->
-     (make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)
-  | None, Some cg ->
-     (make_patt pt,
-      ploc_vala None,
-      <:expr< fun loc -> $cg$ $str:s$ >>)
-  | None, None -> prerr_endline
-      (("Vernac entry \""^s^"\" misses a classifier. "^
-         "A classifier is a function that returns an expression "^
-         "of type vernac_classification (see Vernacexpr). You can: ") ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
-          "new vernacular command does not alter the system state;"))^ "\n" ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
-          "new vernacular command alters the system state but not the "^
-          "parser nor it starts a proof or ends one;"))^ "\n" ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
-          "a global function f.  The function f will be called passing "^
-          "\""^s^"\" as the only argument;")) ^ "\n" ^
-       "- " ^ (
-        "Add a specific classifier in each clause using the syntax:"
-        ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^
-       ("Specific classifiers have precedence over global "^
-         "classifiers. Only one classifier is called.") ^ "\n");
-    (make_patt pt,
-      ploc_vala None,
-      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
-
-let make_fun_clauses loc s l =
+let make_clause_classifier { r_patt = pt; r_class = c; } =
   let map c =
-    let depr = match c.r_depr with
-    | None -> false
-    | Some () -> true
-    in
-    let cl = make_fun loc [make_clause c] in
-    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
+    make_fun loc [(make_patt pt,
+      ploc_vala None,
+      make_let (mk_ignore c pt) pt)]
   in
-  mlexpr_of_list map l
-
-let make_fun_classifiers loc s c l =
-  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
-  mlexpr_of_list (fun x -> x) cl
+  mlexpr_of_option map c
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
@@ -124,23 +83,28 @@ let make_prod_item = function
       <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
       $mlexpr_of_prod_entry_key base g$ ) ) >>
 
-let mlexpr_of_clause cl =
-  let mkexpr { r_head = a; r_patt = b; } = match a with
-  | None -> mlexpr_of_list make_prod_item b
-  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
+| None -> mlexpr_of_list make_prod_item b
+| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+
+let make_rule r =
+  let depr = match r.r_depr with
+  | None -> false
+  | Some () -> true
   in
-  mlexpr_of_list mkexpr cl
+  let gram = mlexpr_of_clause r in
+  let cmd = make_fun loc [make_clause r] in
+  let classif = make_clause_classifier r in
+  <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
-  let gl = mlexpr_of_clause cl in
-  let funcl = make_fun_clauses loc s cl in
-  let classl = make_fun_classifiers loc s c cl in
+  let c = mlexpr_of_option (fun x -> x) c in
+  let rules = mlexpr_of_list make_rule cl in
   declare_str_items loc
     [ <:str_item< do {
-        CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
-        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
-	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
+        Vernacentries.vernac_extend ?{ classifier = $c$ }
+          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
       } >> ]
 
 open Pcaml
@@ -207,7 +171,7 @@ EXTEND
     ] ]
   ;
   classifier:
-    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 6be80d29a5..eca0c6674b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -42,13 +42,6 @@ let string_of_vernac_when = function
 let string_of_vernac_classification (t,w) =
   string_of_vernac_type t ^ " " ^ string_of_vernac_when w
 
-let classifiers = ref []
-let declare_vernac_classifier
-  (s : Vernacexpr.extend_name)
-  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
-=
-  classifiers := !classifiers @ [s,f]
-
 let idents_of_name : Names.Name.t -> Names.Id.t list =
   function
   | Names.Anonymous -> []
@@ -194,7 +187,7 @@ let classify_vernac e =
     | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
-        try List.assoc s !classifiers l ()
+        try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier ~poly = function
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 45fbfb42af..e82b191418 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -9,17 +9,12 @@
 (************************************************************************)
 
 open Vernacexpr
-open Genarg
 
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
 val classify_vernac : vernac_control -> vernac_classification
 
-(** Install a vernacular classifier for VernacExtend *)
-val declare_vernac_classifier :
-  Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
-
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6bc76a2ed..08dd6bec18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2436,3 +2436,52 @@ let interp ?verbosely ?proof ~st cmd =
     let exn = CErrors.push exn in
     Vernacstate.invalidate_cache ();
     iraise exn
+
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+  (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+  classifiers := String.Map.add name f !classifiers
+
+let vernac_extend ~command ?classifier ?entry ext =
+  let get_classifier = function
+  | Some cl -> cl
+  | None ->
+    match classifier with
+    | Some cl -> fun _ -> cl command
+    | None ->
+      let e = match entry with
+      | None -> "COMMAND"
+      | Some e -> Pcoq.Gram.Entry.name e
+      in
+      let msg = Printf.sprintf "\
+        Vernac entry \"%s\" misses a classifier. \
+        A classifier is a function that returns an expression \
+        of type vernac_classification (see Vernacexpr). You can: \n\
+        - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
+          new vernacular command does not alter the system state;\n\
+        - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
+          new vernacular command alters the system state but not the \
+          parser nor it starts a proof or ends one;\n\
+        - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
+          a global function f.  The function f will be called passing\
+          \"%s\" as the only argument;\n\
+        - Add a specific classifier in each clause using the syntax:\n\
+          '[...] => [ f ] -> [...]'.\n\
+        Specific classifiers have precedence over global \
+        classifiers. Only one classifier is called."
+          command e e e command
+      in
+      CErrors.user_err (Pp.strbrk msg)
+  in
+  let cl = Array.map_of_list (fun (_, _, cl, _) -> get_classifier cl) ext in
+  let iter i (depr, f, cl, r) =
+    let () = Vernacinterp.vinterp_add depr (command, i) f in
+    Egramml.extend_vernac_command_grammar (command, i) entry r
+  in
+  let () = declare_vernac_classifier command cl in
+  List.iteri iter ext
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9c05ad8..102f996cf2 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,3 +42,26 @@ val universe_polymorphism_option_name : string list
 (** Elaborate a [atts] record out of a list of flags.
     Also returns whether polymorphism is explicitly (un)set. *)
 val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+
+(** {5 VERNAC EXTEND} *)
+
+type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+
+(** Wrapper to dynamically extend vernacular commands. *)
+val vernac_extend :
+  command:string ->
+  ?classifier:(string -> Vernacexpr.vernac_classification) ->
+  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
+  (bool *
+    Vernacinterp.plugin_args Vernacinterp.vernac_command *
+    classifier option *
+    Vernacexpr.vernac_expr Egramml.grammar_prod_item list) list -> unit
+
+(** {5 STM classifiers} *)
+
+val get_vernac_classifier :
+  Vernacexpr.extend_name -> classifier
+
+(** Low-level API, not for casual user. *)
+val declare_vernac_classifier :
+  string -> classifier array -> unit
-- 
cgit v1.2.3


From b9ff36b39eb193757ce57a89afe138cd09e759d7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Jul 2018 22:57:57 +0200
Subject: Statically typecheck the VERNAC EXTEND wrapper.

This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
---
 grammar/q_util.mli         |   2 +
 grammar/q_util.mlp         |  14 ++++++
 grammar/tacextend.mlp      |  14 ------
 grammar/vernacextend.mlp   | 123 ++++++++++-----------------------------------
 plugins/ltac/tacentries.ml |  11 +---
 vernac/egramml.ml          |   9 ++++
 vernac/egramml.mli         |   2 +
 vernac/vernacentries.ml    |  79 +++++++++++++++++++++++++++--
 vernac/vernacentries.mli   |  15 ++++--
 9 files changed, 140 insertions(+), 129 deletions(-)

diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 323a12357d..f3af318b60 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -48,3 +48,5 @@ val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.ex
 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
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0b8d7fda7a..0e2bf55d86 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -128,3 +128,17 @@ let rec parse_user_entry s sep =
     let s = match s with "hyp" -> "var" | _ -> s in
     check_separator sep;
     Uentry s
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed599..07a9a76139 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -15,20 +15,6 @@ open Argextend
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
-let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
-| Uentry e ->
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f344f3c573..f30c96a7f5 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -14,98 +14,42 @@ open Q_util
 open Argextend
 
 type rule = {
-  r_head : string option;
-  (** The first terminal grammar token *)
   r_patt : extend_token list;
   (** The remaining tokens of the parsing rule *)
   r_class : MLast.expr option;
   (** An optional classifier for the STM *)
   r_branch : MLast.expr;
   (** The action performed by this rule. *)
-  r_depr : unit option;
+  r_depr : bool;
   (** Whether this entry is deprecated *)
 }
 
-(** Quotation difference for match clauses *)
+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 default_patt loc =
-  (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, ploc_vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, Some p) :: l ->
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_let e = function
-  | [] -> e
-  | ExtNonTerminal (g, Some p) :: l ->
-      let t = type_of_user_symbol g in
-      let loc = MLast.loc_of_expr e in
-      let e = make_let e l in
-      <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
-  | _::l -> make_let e l
-
-let make_clause { r_patt = pt; r_branch = e; } =
-  (make_patt pt,
-   ploc_vala None,
-   make_let e pt)
-
-(* To avoid warnings *)
-let mk_ignore c pt =
-  let fold accu = function
-  | ExtNonTerminal (_, Some p) -> p :: accu
-  | _ -> accu
-  in
-  let names = List.fold_left fold [] pt in
-  let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
-  let names = List.fold_left fold <:expr< () >> names in
-  <:expr< do { let _ = $names$ in $c$ } >>
-
-let make_clause_classifier { r_patt = pt; r_class = c; } =
-  let map c =
-    make_fun loc [(make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)]
-  in
-  mlexpr_of_option map c
-
-let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (g, ido) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-    let typ = match ido with None -> None | Some _ -> Some nt in
-      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
-      $mlexpr_of_prod_entry_key base g$ ) ) >>
-
-let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
-| None -> mlexpr_of_list make_prod_item b
-| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+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$) >>
 
 let make_rule r =
-  let depr = match r.r_depr with
-  | None -> false
-  | Some () -> true
-  in
-  let gram = mlexpr_of_clause r in
-  let cmd = make_fun loc [make_clause r] in
-  let classif = make_clause_classifier r in
-  <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
+  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 classif = mlexpr_of_option make_classifier r.r_class in
+  <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
   let c = mlexpr_of_option (fun x -> x) c in
   let rules = mlexpr_of_list make_rule cl in
   declare_str_items loc
-    [ <:str_item< do {
-        Vernacentries.vernac_extend ?{ classifier = $c$ }
-          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
-      } >> ]
+  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
 
 open Pcaml
 
@@ -140,34 +84,21 @@ EXTEND
     ] ]
   ;
   deprecation:
-    [ [ "DEPRECATED" -> () ] ]
+    [ [ -> false | "DEPRECATED" -> true ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string
-      (which otherwise could have been another argument) is not passed
-      to the VernacExtend interpreter function to discriminate between
-      the clauses. *)
   rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+      { r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
+  (** The [OPT "-"] argument serves no purpose nowadays, it is left here for
+      backward compatibility. *)
   fun_rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< $e$ >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< $e$ >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      { r_patt = l; r_class = c; r_branch = e; r_depr = d; }
     ] ]
   ;
   classifier:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a628..463d8633cf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -592,15 +592,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
 let clause_of_ty_ml = function
   | TyML (t,_) -> clause_of_sign t
 
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
-  | TUentry a -> ExtraArg a
-  | TUentryl (a,l) -> ExtraArg a
-  | TUopt(o) -> OptArg (prj o)
-  | TUlist1 l -> ListArg (prj l)
-  | TUlist1sep (l,_) -> ListArg (prj l)
-  | TUlist0 l -> ListArg (prj l)
-  | TUlist0sep (l,_) -> ListArg (prj l)
-
 let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
   fun sign tac ->
     match sign with
@@ -615,7 +606,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
       begin fun tac vals ist -> match vals with
       | [] -> assert false
       | v :: vals ->
-        let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+        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
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 048d4d93a0..c5dedc880e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -64,6 +64,15 @@ let make_rule f prod =
   let act = ty_eval ty_rule f in
   Extend.Rule (symb, act)
 
+let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
+| TUentry a -> ExtraArg a
+| TUentryl (a,l) -> ExtraArg a
+| TUopt(o) -> OptArg (proj_symbol o)
+| TUlist1 l -> ListArg (proj_symbol l)
+| TUlist1sep (l,_) -> ListArg (proj_symbol l)
+| TUlist0 l -> ListArg (proj_symbol l)
+| TUlist0sep (l,_) -> ListArg (proj_symbol l)
+
 (** Vernac grammar extensions *)
 
 let vernac_exts = ref []
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a5ee036db5..c4f4fcfaa4 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -26,6 +26,8 @@ val extend_vernac_command_grammar :
 
 val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
 
+val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
+
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 08dd6bec18..653f8b26e0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2437,8 +2437,75 @@ let interp ?verbosely ?proof ~st cmd =
     Vernacstate.invalidate_cache ();
     iraise exn
 
+(** VERNAC EXTEND registering *)
+
+open Genarg
+open Extend
+
 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
+
+type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
+let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
+
+let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
+| TyNil -> fun f args ->
+  begin match args with
+  | [] -> f
+  | _ :: _ -> type_error ()
+  end
+| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+  begin match args with
+  | [] -> type_error ()
+  | Genarg.GenArg (Rawwit tag, v) :: args ->
+    match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+    | None -> type_error ()
+    | Some Refl -> untype_classifier ty (f v) args
+  end
+
+(** Stupid GADTs forces us to duplicate the definition just for typing *)
+let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function
+| TyNil -> fun f args ->
+  begin match args with
+  | [] -> f
+  | _ :: _ -> type_error ()
+  end
+| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
+| TyNonTerminal (_, tu, ty) -> fun f args ->
+  begin match args with
+  | [] -> type_error ()
+  | Genarg.GenArg (Rawwit tag, v) :: args ->
+    match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
+    | None -> type_error ()
+    | Some Refl -> untype_command ty (f v) args
+  end
+
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function
+| TUlist1 l -> Alist1 (untype_user_symbol l)
+| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUlist0 l -> Alist0 (untype_user_symbol l)
+| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
+| TUopt o -> Aopt (untype_user_symbol o)
+| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a))
+| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i)
+
+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
+  let symb = untype_user_symbol tu in
+  Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
+
+let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
+
 let classifiers : classifier array String.Map.t ref = ref String.Map.empty
 
 let get_vernac_classifier (name, i) args =
@@ -2448,8 +2515,8 @@ let declare_vernac_classifier name f =
   classifiers := String.Map.add name f !classifiers
 
 let vernac_extend ~command ?classifier ?entry ext =
-  let get_classifier = function
-  | Some cl -> cl
+  let get_classifier (TyML (_, ty, _, cl)) = match cl with
+  | Some cl -> untype_classifier ty cl
   | None ->
     match classifier with
     | Some cl -> fun _ -> cl command
@@ -2478,9 +2545,11 @@ let vernac_extend ~command ?classifier ?entry ext =
       in
       CErrors.user_err (Pp.strbrk msg)
   in
-  let cl = Array.map_of_list (fun (_, _, cl, _) -> get_classifier cl) ext in
-  let iter i (depr, f, cl, r) =
-    let () = Vernacinterp.vinterp_add depr (command, i) f in
+  let cl = Array.map_of_list get_classifier ext in
+  let iter i (TyML (depr, ty, f, _)) =
+    let f = untype_command ty f in
+    let r = untype_grammar ty in
+    let () = vinterp_add depr (command, i) f in
     Egramml.extend_vernac_command_grammar (command, i) entry r
   in
   let () = declare_vernac_classifier command cl in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 102f996cf2..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -47,15 +47,22 @@ val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool o
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
+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
+
+type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml
+
 (** Wrapper to dynamically extend vernacular commands. *)
 val vernac_extend :
   command:string ->
   ?classifier:(string -> Vernacexpr.vernac_classification) ->
   ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
-  (bool *
-    Vernacinterp.plugin_args Vernacinterp.vernac_command *
-    classifier option *
-    Vernacexpr.vernac_expr Egramml.grammar_prod_item list) list -> unit
+  ty_ml list -> unit
 
 (** {5 STM classifiers} *)
 
-- 
cgit v1.2.3