Merge PR #8050: Cleanup VERNAC EXTEND

11 files changed, 210 insertions, 175 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 02da61ef77..07239e7af0 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 a2872d07f6..f30c96a7f5 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -14,134 +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 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 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 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$)>>
-  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
-
-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 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)
-  in
-  mlexpr_of_list mkexpr cl
+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$) >>
+
+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 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 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$;
-      } >> ]
+  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
 
 open Pcaml
 
@@ -176,38 +84,25 @@ 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:
-    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4b834d66d3..636cb8ebf8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -594,15 +594,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
@@ -617,7 +608,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/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/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 b6bc76a2ed..653f8b26e0 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2436,3 +2436,121 @@ let interp ?verbosely ?proof ~st cmd =
     let exn = CErrors.push exn in
     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 =
+  (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 (TyML (_, ty, _, cl)) = match cl with
+  | Some cl -> untype_classifier ty 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 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
+  List.iteri iter ext
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9c05ad8..fb2a30bac7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -42,3 +42,33 @@ 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
+
+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 ->
+  ty_ml 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