[camlp5] Remove dependency on camlp5.

6 files changed, 0 insertions, 653 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
deleted file mode 100644
index 715b8cd23f..0000000000
--- a/grammar/argextend.mlp
+++ /dev/null
@@ -1,221 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Q_util
-
-let loc = Ploc.dummy
-
-IFDEF STRICT THEN
-  let ploc_vala x = Ploc.VaVal x
-ELSE
-  let ploc_vala x = x
-END
-
-let declare_str_items loc l =
-  MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
-
-let declare_arg loc s e =
-  declare_str_items loc [
-    <:str_item< value ($lid:"wit_"^s$, $lid:s$) = $e$ >>;
-    (** Prevent the unused variable warning *)
-    <:str_item< value _ = ($lid:"wit_"^s$, $lid:s$) >>;
-  ]
-
-let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
-
-let rec make_wit loc = function
-  | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
-  | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
-  | PairArgType (t1,t2) ->
-      <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
-  | ExtraArgType s -> mk_extraarg loc s
-
-let is_self s = function
-| ExtraArgType s' -> s = s'
-| _ -> false
-
-let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
-let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
-let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
-
-let make_act loc act pil =
-  let rec make = function
-    | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
-    | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
-    | ExtTerminal _ :: tl ->
-	<:expr< (fun _ -> $make tl$) >> in
-  make (List.rev pil)
-
-let make_prod_item self = function
-  | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (Uentry e, _) when e = self -> <:expr< Extend.Aself >>
-  | ExtNonTerminal (g, _) ->
-    let base s = <:expr< $lid:s$ >> in
-    mlexpr_of_prod_entry_key base g
-
-let rec make_prod self = function
-| [] -> <:expr< Extend.Stop >>
-| item :: prods -> <:expr< Extend.Next $make_prod self prods$ $make_prod_item self item$ >>
-
-let make_rule loc self (prods,act) =
-  <:expr< Extend.Rule $make_prod self (List.rev prods)$ $make_act loc act prods$ >>
-
-let is_ident x = function
-| <:expr< $lid:s$ >> -> (s : string) = x
-| _ -> false
-
-let make_extend loc self cl = match cl with
-| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
-  (** Special handling of identity arguments by not redeclaring an entry *)
-  <:expr< Vernacextend.Arg_alias $lid:e$ >>
-| _ ->
-  <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >>
-
-let warning_deprecated prefix s = function
-| None -> ()
-| Some _ ->
-  Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \
-                  Use [TYPED AS] instead.\n%!" prefix s
-
-let get_type s = function
-| None -> None
-| Some typ ->
-  if is_self s typ then
-    let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in
-    None
-  else Some typ
-
-let declare_tactic_argument loc s (typ, f, g, h) cl =
-  let se = mlexpr_of_string s in
-  let typ, pr = match typ with
-    | `Uniform (typ, pr) ->
-      let typ = get_type s typ in
-      typ, <:expr< ($lid:pr$, $lid:pr$, $lid:pr$) >>
-    | `Specialized (a, rpr, c, gpr, e, tpr) ->
-      let () = warning_deprecated "RAW_" s a in
-      let () = warning_deprecated "GLOB_" s c in
-      let typ = get_type s e in
-      typ, <:expr< ($lid:rpr$, $lid:gpr$, $lid:tpr$) >>
-  in
-  let glob = match g, typ with
-  | Some f, (None | Some _) ->
-    <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, $lid:f$ ist v)) >>
-  | None, Some typ ->
-    <:expr< Tacentries.ArgInternWit $make_wit loc typ$ >>
-  | None, None ->
-    <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, v)) >>
-  in
-  let interp = match f, typ with
-  | Some f, (None | Some _) ->
-    <:expr< Tacentries.ArgInterpLegacy $lid:f$ >>
-  | None, Some typ ->
-    <:expr< Tacentries.ArgInterpWit $make_wit loc typ$ >>
-  | None, None ->
-    <:expr< Tacentries.ArgInterpRet >>
-  in
-  let subst = match h, typ with
-  | Some f, (None | Some _) ->
-    <:expr< Tacentries.ArgSubstFun $lid:f$ >>
-  | None, Some typ ->
-    <:expr< Tacentries.ArgSubstWit $make_wit loc typ$ >>
-  | None, None ->
-    <:expr< Tacentries.ArgSubstFun (fun s v -> v) >>
-  in
-  let dyn = mlexpr_of_option (fun typ -> <:expr< Geninterp.val_tag $make_topwit loc typ$ >>) typ in
-  declare_arg loc s <:expr< Tacentries.argument_extend ~{ name = $se$ } {
-    Tacentries.arg_parsing = $make_extend loc s cl$;
-    Tacentries.arg_tag = $dyn$;
-    Tacentries.arg_intern = $glob$;
-    Tacentries.arg_subst = $subst$;
-    Tacentries.arg_interp = $interp$;
-    Tacentries.arg_printer = $pr$
-  } >>
-
-let declare_vernac_argument loc s pr cl =
-  let se = mlexpr_of_string s in
-  let pr_rules = match pr with
-    | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >>
-    | Some pr -> <:expr< $lid:pr$ >> in
-  declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } {
-    Vernacextend.arg_printer = $pr_rules$;
-    Vernacextend.arg_parsing = $make_extend loc s cl$
-  } >>
-
-open Pcaml
-
-EXTEND
-  GLOBAL: str_item;
-  str_item:
-    [ [ "ARGUMENT"; "EXTEND"; s = entry_name;
-        header = argextend_header;
-        OPT "|"; l = LIST1 argrule SEP "|";
-        "END" ->
-         declare_tactic_argument loc s header l
-      | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name;
-        pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
-        OPT "|"; l = LIST1 argrule SEP "|";
-        "END" ->
-         declare_vernac_argument loc s pr l ] ]
-  ;
-  argextend_specialized:
-  [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ];
-      "RAW_PRINTED"; "BY"; rawpr = LIDENT;
-      globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ];
-      "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
-      (rawtyp, rawpr, globtyp, globpr) ] ]
-  ;
-  argextend_header:
-    [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ];
-        "PRINTED"; "BY"; pr = LIDENT;
-        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
-        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
-        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
-        special = OPT argextend_specialized ->
-        let repr = match special with
-        | None -> `Uniform (typ, pr)
-        | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr)
-        in
-        (repr, f, g, h) ] ]
-  ;
-  argtype:
-    [ "2"
-      [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
-    | "1"
-      [ e = argtype; LIDENT "list" -> ListArgType e
-      | e = argtype; LIDENT "option" -> OptArgType e ]
-    | "0"
-      [ e = LIDENT ->
-        let e = parse_user_entry e "" in
-        type_of_user_symbol e
-      | "("; e = argtype; ")" -> e ] ]
-  ;
-  argrule:
-    [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
-  ;
-  genarg:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let e = parse_user_entry e sep in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, None)
-      | s = STRING -> ExtTerminal s
-    ] ]
-  ;
-  entry_name:
-    [ [ s = LIDENT -> s
-      | UIDENT -> failwith "Argument entry names must be lowercase"
-      ] ]
-  ;
-  END
diff --git a/grammar/dune b/grammar/dune
deleted file mode 100644
index 78df2826d6..0000000000
--- a/grammar/dune
+++ /dev/null
@@ -1,41 +0,0 @@
-(library
- (name grammar5)
- (synopsis "Coq Camlp5 Grammar Extensions for Plugins")
- (public_name coq.grammar)
- (flags (:standard -w -58))
- (libraries camlp5))
-
-; Custom camlp5! This is a net speedup, and a preparation for using
-; Dune's preprocessor abilities.
-(rule
- (targets coqmlp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx -o coqmlp5)))
-
-(rule
- (targets coqp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5)))
-
-(install
- (section bin)
- (package coq)
- (files coqp5 coqmlp5))
-
-(rule
- (targets q_util.ml)
- (deps (:mlp-file q_util.mlp))
- (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
-
-(rule
- (targets argextend.ml)
- (deps (:mlp-file argextend.mlp))
- (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
-
-(rule
- (targets tacextend.ml)
- (deps (:mlp-file tacextend.mlp))
- (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
-
-(rule
- (targets vernacextend.ml)
- (deps (:mlp-file vernacextend.mlp))
- (action (run coqmlp5 -loc loc -impl %{mlp-file} -o %{targets})))
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
deleted file mode 100644
index b163100fc3..0000000000
--- a/grammar/q_util.mli
+++ /dev/null
@@ -1,54 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-type argument_type =
-| ListArgType of argument_type
-| OptArgType of argument_type
-| PairArgType of argument_type * argument_type
-| ExtraArgType of string
-
-type user_symbol =
-| Ulist1 of user_symbol
-| Ulist1sep of user_symbol * string
-| Ulist0 of user_symbol
-| Ulist0sep of user_symbol * string
-| Uopt of user_symbol
-| Uentry of string
-| Uentryl of string * int
-
-type extend_token =
-| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string option
-
-val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
-
-val mlexpr_of_pair :
-  ('a -> MLast.expr) -> ('b -> MLast.expr)
-    -> 'a * 'b -> MLast.expr
-
-val mlexpr_of_bool : bool -> MLast.expr
-
-val mlexpr_of_int : int -> MLast.expr
-
-val mlexpr_of_string : string -> MLast.expr
-
-val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
-
-val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr
-
-val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
-
-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
deleted file mode 100644
index a2007d258c..0000000000
--- a/grammar/q_util.mlp
+++ /dev/null
@@ -1,150 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* This file defines standard combinators to build ml expressions *)
-
-type argument_type =
-| ListArgType of argument_type
-| OptArgType of argument_type
-| PairArgType of argument_type * argument_type
-| ExtraArgType of string
-
-type user_symbol =
-| Ulist1 of user_symbol
-| Ulist1sep of user_symbol * string
-| Ulist0 of user_symbol
-| Ulist0sep of user_symbol * string
-| Uopt of user_symbol
-| Uentry of string
-| Uentryl of string * int
-
-type extend_token =
-| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string option
-
-let mlexpr_of_list f l =
-  List.fold_right
-    (fun e1 e2 ->
-      let e1 = f e1 in
-       let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
-       <:expr< [$e1$ :: $e2$] >>)
-    l (let loc = Ploc.dummy in <:expr< [] >>)
-
-let mlexpr_of_pair m1 m2 (a1,a2) =
-  let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
-  <:expr< ($e1$, $e2$) >>
-
-(* We don't give location for tactic quotation! *)
-let loc = Ploc.dummy
-
-
-let mlexpr_of_bool = function
-  | true -> <:expr< True >>
-  | false -> <:expr< False >>
-
-let mlexpr_of_int n = <:expr< $int:string_of_int n$ >>
-
-let mlexpr_of_string s = <:expr< $str:s$ >>
-
-let mlexpr_of_option f = function
-  | None -> <:expr< None >>
-  | Some e -> <:expr< Some $f e$ >>
-
-let mlexpr_of_name f = function
-  | None -> <:expr< Names.Name.Anonymous >>
-  | Some e -> <:expr< Names.Name.Name $f e$ >>
-
-let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
-
-let rec mlexpr_of_prod_entry_key f = function
-  | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
-  | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
-  | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Uentry e -> <:expr< Extend.Aentry ($f e$) >>
-  | Uentryl (e, l) ->
-    (** Keep in sync with Pcoq! *)
-    assert (e = "tactic");
-    if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >>
-    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_string (string_of_int l)$ >>
-
-let rec type_of_user_symbol = function
-| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
-  ListArgType (type_of_user_symbol s)
-| Uopt s ->
-  OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) -> ExtraArgType e
-
-let coincide s pat off =
-  let len = String.length pat in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = Char.code s.[off + !i] in
-    let d = Char.code pat.[!i] in
-    break := c = d;
-    incr i
-  done;
-  !break
-
-let check_separator sep =
-  if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep."
-
-let rec parse_user_entry s sep =
-  let l = String.length s in
-  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
-    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
-    check_separator sep;
-    Ulist1 entry
-  else if l > 12 && coincide s "ne_" 0 &&
-                   coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
-    Ulist1sep (entry, sep)
-  else if l > 5 && coincide s "_list" (l-5) then
-    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
-    check_separator sep;
-    Ulist0 entry
-  else if l > 9 && coincide s "_list_sep" (l-9) then
-    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
-    Ulist0sep (entry, sep)
-  else if l > 4 && coincide s "_opt" (l-4) then
-    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
-    check_separator sep;
-    Uopt entry
-  else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
-    let n = Char.code s.[6] - 48 in
-    check_separator sep;
-    Uentryl ("tactic", n)
-  else
-    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$>>
-
-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
deleted file mode 100644
index a093f78388..0000000000
--- a/grammar/tacextend.mlp
+++ /dev/null
@@ -1,72 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** WARNING: this file is deprecated; consider modifying coqpp instead. *)
-
-(** Implementation of the TACTIC EXTEND macro. *)
-
-open Q_util
-open Argextend
-
-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, _) :: cl ->
-  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
-
-open Pcaml
-
-EXTEND
-  GLOBAL: str_item;
-  str_item:
-    [ [ "TACTIC"; "EXTEND"; s = tac_name;
-        depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
-        level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
-        OPT "|"; l = LIST1 tacrule SEP "|";
-        "END" ->
-        let level = match level with Some i -> int_of_string i | None -> 0 in
-        let level = mlexpr_of_int level in
-        let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
-        let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
-        declare_str_items loc [ <:str_item< Tacentries.tactic_extend
-          $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
-          $depr$ } $l$ >> ] ] ]
-  ;
-  tacrule:
-    [ [ "["; l = LIST1 tacargs; "]";
-        "->"; "["; e = Pcaml.expr; "]" ->
-        let e = <:expr< fun ist -> $e$ >> in
-         <:expr< TyML($mlexpr_of_clause l$, $binders_of_tokens e l$) >>
-    ] ]
-  ;
-
-  tacargs:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let e = parse_user_entry e sep in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, None)
-      | s = STRING ->
-	let () = if s = "" then failwith "Empty terminal." in
-        ExtTerminal s
-    ] ]
-  ;
-  tac_name:
-    [ [ s = LIDENT -> s
-      | s = UIDENT -> s
-    ] ]
-  ;
-  END
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
deleted file mode 100644
index d44eeef670..0000000000
--- a/grammar/vernacextend.mlp
+++ /dev/null
@@ -1,115 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Implementation of the VERNAC EXTEND macro. *)
-
-open Q_util
-open Argextend
-
-type rule = {
-  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 : bool;
-  (** Whether this entry is deprecated *)
-}
-
-let rec mlexpr_of_clause = function
-| [] -> <:expr< Vernacextend.TyNil >>
-| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
-| ExtNonTerminal (g, id) :: cl ->
-  <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
-
-let make_rule r =
-  let ty = mlexpr_of_clause 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< Vernacextend.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< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
-
-open Pcaml
-
-EXTEND
-  GLOBAL: str_item;
-  str_item:
-    [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification;
-        OPT "|"; l = LIST1 rule SEP "|";
-        "END" ->
-         declare_command loc s c <:expr<None>> l
-      | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification;
-        OPT "|"; l = LIST1 fun_rule SEP "|";
-        "END" ->
-         declare_command loc s c <:expr<None>> l
-      | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
-        OPT "|"; l = LIST1 rule SEP "|";
-        "END" ->
-          declare_command loc s c <:expr<Some $lid:nt$>> l
-      | "DECLARE"; "PLUGIN"; name = STRING ->
-        declare_str_items loc [
-          <:str_item< value __coq_plugin_name = $str:name$ >>;
-          <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
-        ]
-      ] ]
-  ;
-  classification:
-    [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >>
-      | "CLASSIFIED"; "AS"; "SIDEFF" ->
-          <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >>
-      | "CLASSIFIED"; "AS"; "QUERY" ->
-          <:expr< fun _ -> Vernac_classifier.classify_as_query >>
-    ] ]
-  ;
-  deprecation:
-    [ [ -> false | "DEPRECATED" -> true ] ]
-  ;
-  rule:
-    [ [ "["; OPT "-"; l = LIST1 args; "]";
-        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { 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:
-    [ [ "["; 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< $c$>> ] ]
-  ;
-  args:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let e = parse_user_entry e sep in
-        ExtNonTerminal (e, Some s)
-      | e = LIDENT ->
-        let e = parse_user_entry e "" in
-        ExtNonTerminal (e, None)
-      | s = STRING ->
-        ExtTerminal s
-    ] ]
-  ;
-  END
-;;