place all files specific to camlp4 syntax extensions in grammar/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 2 insertions, 1513 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
deleted file mode 100644
index 5a64580d2..000000000
--- a/parsing/argextend.ml4
+++ /dev/null
@@ -1,340 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
-open Genarg
-open Q_util
-open Egramml
-open Pcoq
-open Compat
-
-let loc = Pp.dummy_loc
-let default_loc = <:expr< Pp.dummy_loc >>
-
-let rec make_rawwit loc = function
-  | BoolArgType -> <:expr< Genarg.rawwit_bool >>
-  | IntArgType -> <:expr< Genarg.rawwit_int >>
-  | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >>
-  | StringArgType -> <:expr< Genarg.rawwit_string >>
-  | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
-  | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
-  | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >>
-  | VarArgType -> <:expr< Genarg.rawwit_var >>
-  | RefArgType -> <:expr< Genarg.rawwit_ref >>
-  | SortArgType -> <:expr< Genarg.rawwit_sort >>
-  | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
-  | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
-  | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
-  | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
-  | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
-  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
-  | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >>
-  | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
-  | PairArgType (t1,t2) ->
-      <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >>
-  | ExtraArgType s ->
-    <:expr<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"rawwit_"^s$;
-      end in WIT.wit >>
-
-let rec make_globwit loc = function
-  | BoolArgType -> <:expr< Genarg.globwit_bool >>
-  | IntArgType -> <:expr< Genarg.globwit_int >>
-  | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >>
-  | StringArgType -> <:expr< Genarg.globwit_string >>
-  | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
-  | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
-  | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >>
-  | VarArgType -> <:expr< Genarg.globwit_var >>
-  | RefArgType -> <:expr< Genarg.globwit_ref >>
-  | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
-  | SortArgType -> <:expr< Genarg.globwit_sort >>
-  | ConstrArgType -> <:expr< Genarg.globwit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
-  | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
-  | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
-  | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
-  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
-  | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >>
-  | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >>
-  | PairArgType (t1,t2) ->
-      <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >>
-  | ExtraArgType s ->
-    <:expr<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"globwit_"^s$;
-      end in WIT.wit >>
-
-let rec make_wit loc = function
-  | BoolArgType -> <:expr< Genarg.wit_bool >>
-  | IntArgType -> <:expr< Genarg.wit_int >>
-  | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
-  | StringArgType -> <:expr< Genarg.wit_string >>
-  | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
-  | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
-  | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >>
-  | VarArgType -> <:expr< Genarg.wit_var >>
-  | RefArgType -> <:expr< Genarg.wit_ref >>
-  | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
-  | SortArgType -> <:expr< Genarg.wit_sort >>
-  | ConstrArgType -> <:expr< Genarg.wit_constr >>
-  | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
-  | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
-  | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
-  | BindingsArgType -> <:expr< Genarg.wit_bindings >>
-  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
-  | List1ArgType t -> <:expr< Genarg.wit_list1 $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 ->
-    <:expr<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"wit_"^s$;
-      end in WIT.wit >>
-
-let has_extraarg =
-  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
-
-let statically_known_possibly_empty s (prods,_) =
-  List.for_all (function
-    | GramNonTerminal(_,ExtraArgType s',_,_) ->
-        (* For ExtraArg we don't know (we'll have to test dynamically) *)
-        (* unless it is a recursive call *)
-        s <> s'
-    | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) ->
-        (* Opt and List0 parses the empty string *)
-        true
-    | _ ->
-        (* This consumes a token for sure *) false)
-      prods
-
-let possibly_empty_subentries loc (prods,act) =
-  let bind_name p v e = match p with
-    | None -> e
-    | Some id ->
-        let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
-  let rec aux = function
-    | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >>
-    | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
-        bind_name p <:expr< None >> (aux tl)
-    | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
-        bind_name p <:expr< [] >> (aux tl)
-    | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
-        (* We check at runtime if extraarg s parses "epsilon" *)
-        let s = match p with None -> "_" | Some id -> Names.string_of_id id in
-        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with
-          [ None -> raise Exit
-          | Some v -> v ] in $aux tl$ >>
-    | _ -> assert false (* already filtered out *) in
-  if has_extraarg prods then
-    (* Needs a dynamic check; catch all exceptions if ever some rhs raises *)
-    (* an exception rather than returning a value; *)
-    (* declares loc because some code can refer to it; *)
-    (* ensures loc is used to avoid "unused variable" warning *)
-    (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
-  else
-    (* Static optimisation *)
-    (false, aux prods)
-
-let make_possibly_empty_subentries loc s cl =
-  let cl = List.filter (statically_known_possibly_empty s) cl in
-  if cl = [] then
-    <:expr< None >>
-  else
-    let rec aux = function
-    | (true, e) :: l ->
-        <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
-    | (false, e) :: _ ->
-        <:expr< Some $e$ >>
-    | [] ->
-        <:expr< None >> in
-    aux (List.map (possibly_empty_subentries loc) cl)
-
-let make_act loc act pil =
-  let rec make = function
-    | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
-    | GramNonTerminal (_,t,_,Some p) :: tl ->
-	let p = Names.string_of_id p in
-	<:expr<
-          Pcoq.Gram.action
-            (fun $lid:p$ ->
-               let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
-        >>
-    | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl ->
-	<:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in
-  make (List.rev pil)
-
-let make_prod_item = function
-  | GramTerminal s -> <:expr< Pcoq.gram_token_of_string $str:s$ >>
-  | GramNonTerminal (_,_,g,_) ->
-      <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >>
-
-let make_rule loc (prods,act) =
-  <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >>
-
-let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
-  let rawtyp, rawpr, globtyp, globpr = match typ with
-    | `Uniform typ -> typ, pr, typ, pr
-    | `Specialized (a, b, c, d) -> a, b, c, d
-  in
-  let glob = match g with
-    | None ->
-	<:expr< fun e x ->
-          out_gen $make_globwit loc rawtyp$
-            (Tacinterp.intern_genarg e
-               (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >>
-    | Some f -> <:expr< $lid:f$>> in
-  let interp = match f with
-    | None ->
-	<:expr< fun ist gl x ->
-	  let (sigma,a_interp) =
-	    Tacinterp.interp_genarg ist gl
-               (Genarg.in_gen $make_globwit loc globtyp$ x)
-	  in
-          (sigma , out_gen $make_wit loc globtyp$ a_interp)>>
-    | Some f -> <:expr< $lid:f$>> in
-  let substitute = match h with
-    | None ->
-	<:expr< fun s x ->
-          out_gen $make_globwit loc globtyp$
-	    (Tacinterp.subst_genarg s
-               (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
-    | Some f -> <:expr< $lid:f$>> in
-  let se = mlexpr_of_string s in
-  let wit = <:expr< $lid:"wit_"^s$ >> in
-  let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
-  let globwit = <:expr< $lid:"globwit_"^s$ >> in
-  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
-  let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
-  declare_str_items loc
-   [ <:str_item<
-      value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
-      Genarg.create_arg $default_value$ $se$>>;
-     <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
-     <:str_item< do {
-      Tacinterp.add_interp_genarg $se$
-        ((fun e x ->
-          (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
-        (fun ist gl x ->
-	  let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in
-          (sigma , Genarg.in_gen $wit$ a_interp)),
-        (fun subst x ->
-          (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
-      Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
-	(None, [(None, None, $rules$)]);
-      Pptactic.declare_extra_genarg_pprule
-        ($rawwit$, $lid:rawpr$)
-        ($globwit$, $lid:globpr$)
-        ($wit$, $lid:pr$) }
-     >> ]
-
-let declare_vernac_argument loc s pr cl =
-  let se = mlexpr_of_string s in
-  let wit = <:expr< $lid:"wit_"^s$ >> in
-  let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
-  let globwit = <:expr< $lid:"globwit_"^s$ >> in
-  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
-  let pr_rules = match pr with
-    | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
-    | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
-  declare_str_items loc
-   [ <:str_item<
-      value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
-             ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
-              $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>;
-     <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
-    <:str_item< do {
-      Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
-	(None, [(None, None, $rules$)]);
-      Pptactic.declare_extra_genarg_pprule
-        ($rawwit$, $pr_rules$)
-        ($globwit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer")
-        ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") }
-      >> ]
-
-open Vernacexpr
-open Pcoq
-open Pcaml
-open PcamlSig
-
-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_header:
-    [ [ "TYPED"; "AS"; typ = argtype;
-        "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 ] ->
-        (`Uniform typ, pr, f, g, h)
-      | "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 ];
-        "RAW_TYPED"; "AS"; rawtyp = argtype;
-        "RAW_PRINTED"; "BY"; rawpr = LIDENT;
-        "GLOB_TYPED"; "AS"; globtyp = argtype;
-        "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
-        (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ]
-  ;
-  argtype:
-    [ "2"
-      [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
-    | "1"
-      [ e = argtype; LIDENT "list" -> List0ArgType e
-      | e = argtype; LIDENT "option" -> OptArgType e ]
-    | "0"
-      [ e = LIDENT -> fst (interp_entry_name false None e "")
-      | "("; e = argtype; ")" -> e ] ]
-  ;
-  argrule:
-    [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
-  ;
-  genarg:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
-	GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
-	GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | s = STRING ->
-	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Lexer.add_keyword s;
-          GramTerminal s
-    ] ]
-  ;
-  entry_name:
-    [ [ s = LIDENT -> s
-      | UIDENT -> failwith "Argument entry names must be lowercase"
-      ] ]
-  ;
-  END
-
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index d763a1cab..d4229ff0b 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 (*
   Syntax for the subtac terms and types.
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
deleted file mode 100644
index 313676c96..000000000
--- a/parsing/grammar.mllib
+++ /dev/null
@@ -1,38 +0,0 @@
-Coq_config
-
-Pp_control
-Compat
-Flags
-Pp
-Segmenttree
-Unicodetable
-Errors
-Util
-Bigint
-Hashcons
-Predicate
-Option
-
-Names
-Libnames
-Genarg
-Tok
-Lexer
-Extend
-Extrawit
-Pcoq
-Q_util
-Q_coqast
-
-Egramml
-Argextend
-Tacextend
-Vernacextend
-
-Redops
-Constrexpr_ops
-Locusops
-G_prim
-G_tactic
-G_ltac
-G_constr
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 6ccbdb752..13ed80464 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -4,4 +4,4 @@ G_prim
 G_proofs
 G_tactic
 G_ltac
-G_obligations
\ No newline at end of file
+G_obligations
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
deleted file mode 100644
index d78b6c8c0..000000000
--- a/parsing/q_constr.ml4
+++ /dev/null
@@ -1,127 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
-open Glob_term
-open Term
-open Names
-open Pattern
-open Q_util
-open Pp
-open Compat
-open Pcaml
-open PcamlSig
-open Misctypes
-
-let loc = dummy_loc
-let dloc = <:expr< Pp.dummy_loc >>
-
-let apply_ref f l =
-  <:expr<
-    Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
-  >>
-
-EXTEND
-  GLOBAL: expr;
-  expr:
-    [ [ "PATTERN"; "["; c = constr; "]" ->
-      <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
-  ;
-  sort:
-    [ [ "Set"  -> GSet
-      | "Prop" -> GProp
-      | "Type" -> GType None ] ]
-  ;
-  ident:
-    [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]
-  ;
-  name:
-    [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ]
-  ;
-  string:
-    [ [ s = UIDENT -> s | s = LIDENT -> s ] ]
-  ;
-  constr:
-    [ "200" RIGHTA
-      [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
-        <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
-      | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
-        <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
-      | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
-        <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
-      (* fix todo *)
-      ]
-    | "100" RIGHTA
-      [ c1 = constr; ":"; c2 = SELF ->
-        <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
-    | "90" RIGHTA
-      [ c1 = constr; "->"; c2 = SELF ->
-        <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ]
-    | "75" RIGHTA
-      [ "~"; c = constr ->
-        apply_ref <:expr< coq_not_ref >> [c] ]
-    | "70" RIGHTA
-      [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT ->
-        apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ]
-    | "10" LEFTA
-      [ f = constr; args = LIST1 NEXT ->
-        let args = mlexpr_of_list (fun x -> x) args in
-        <:expr< Glob_term.GApp ($dloc$,$f$,$args$) >> ]
-    | "0"
-      [ s = sort -> <:expr< Glob_term.GSort ($dloc$,s) >>
-      | id = ident -> <:expr< Glob_term.GVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Glob_term.GHole ($dloc$,Evar_kinds.QuestionMark (Evar_kinds.Define False)) >>
-      | "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >>
-      | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
-          apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
-      | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >>
-      | c = match_constr -> c
-      | "("; c = constr LEVEL "200"; ")" -> c ] ]
-  ;
-  match_constr:
-    [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type;
-        "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" ->
-          let br = mlexpr_of_list (fun x -> x) br in
-     <:expr< Glob_term.GCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >>
-    ] ]
-  ;
-  match_type:
-    [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name;
-        "return"; ty = constr LEVEL "100" ->
-          let nal = mlexpr_of_list (fun x -> x) nal in
-          <:expr< Some $ty$ >>,
-          <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >>
-      | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ]
-  ;
-  eqn:
-    [ [ (lid,pl) = pattern; "=>"; rhs = constr ->
-        let lid = mlexpr_of_list (fun x -> x) lid in
-        <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >>
-    ] ]
-  ;
-  pattern:
-    [ [ "%"; e = string; lip = LIST0 patvar ->
-        let lp = mlexpr_of_list (fun (_,x) -> x) lip in
-        let lid = List.flatten (List.map fst lip) in
-        lid, <:expr< Glob_term.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >>
-      | p = patvar -> p
-      | "("; p = pattern; ")" -> p ] ]
-  ;
-  patvar:
-    [ [ "_" -> [], <:expr< Glob_term.PatVar ($dloc$,Anonymous) >>
-      | id = ident -> [id], <:expr< Glob_term.PatVar ($dloc$,Name $id$) >>
-    ] ]
-  ;
-  END;;
-
-(* Example
-open Coqlib
-let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ]
-*)
-
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
deleted file mode 100644
index 7467a32f0..000000000
--- a/parsing/q_coqast.ml4
+++ /dev/null
@@ -1,568 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Names
-open Q_util
-open Compat
-
-let is_meta s = String.length s > 0 && s.[0] == '$'
-
-let purge_str s =
-  if String.length s == 0 || s.[0] <> '$' then s
-  else String.sub s 1 (String.length s - 1)
-
-let anti loc x =
-  expl_anti loc <:expr< $lid:purge_str x$ >>
-
-(* We don't give location for tactic quotation! *)
-let loc = dummy_loc
-
-let dloc = <:expr< Pp.dummy_loc >>
-
-let mlexpr_of_ident id =
-  <:expr< Names.id_of_string $str:Names.string_of_id id$ >>
-
-let mlexpr_of_name = function
-  | Names.Anonymous -> <:expr< Names.Anonymous >>
-  | Names.Name id ->
-      <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >>
-
-let mlexpr_of_dirpath dir =
-  let l = Names.repr_dirpath dir in
-  <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >>
-
-let mlexpr_of_qualid qid =
-  let (dir, id) = Libnames.repr_qualid qid in
-  <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
-
-let mlexpr_of_reference = function
-  | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
-  | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
-
-let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
-
-let mlexpr_of_loc loc = <:expr< $dloc$ >>
-
-let mlexpr_of_by_notation f = function
-  | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >>
-  | Misctypes.ByNotation (loc,s,sco) ->
-      <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
-
-let mlexpr_of_intro_pattern = function
-  | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >>
-  | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
-  | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
-  | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
-  | Misctypes.IntroIdentifier id ->
-      <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
-  | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ ->
-      failwith "mlexpr_of_intro_pattern: TODO"
-
-let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
-
-let mlexpr_of_or_metaid f = function
-  | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >>
-  | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >>
-
-let mlexpr_of_quantified_hypothesis = function
-  | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
-  | Misctypes.NamedHyp id ->  <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
-
-let mlexpr_of_or_var f = function
-  | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
-  | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
-
-let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
-
-let mlexpr_of_occs = function
-  | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
-  | Locus.AllOccurrencesBut l ->
-    <:expr< Locus.AllOccurrencesBut
-      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
-  | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >>
-  | Locus.OnlyOccurrences l ->
-    <:expr< Locus.OnlyOccurrences
-      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
-
-let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
-
-let mlexpr_of_hyp_location = function
-  | occs, Locus.InHyp ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >>
-  | occs, Locus.InHypTypeOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >>
-  | occs, Locus.InHypValueOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >>
-
-let mlexpr_of_clause cl =
-  <:expr< {Locus.onhyps=
-             $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
-               cl.Locus.onhyps$;
-           Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
-
-let mlexpr_of_red_flags {
-  Genredexpr.rBeta = bb;
-  Genredexpr.rIota = bi;
-  Genredexpr.rZeta = bz;
-  Genredexpr.rDelta = bd;
-  Genredexpr.rConst = l
-} = <:expr< {
-  Genredexpr.rBeta = $mlexpr_of_bool bb$;
-  Genredexpr.rIota = $mlexpr_of_bool bi$;
-  Genredexpr.rZeta = $mlexpr_of_bool bz$;
-  Genredexpr.rDelta = $mlexpr_of_bool bd$;
-  Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
-} >>
-
-let mlexpr_of_explicitation = function
-  | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >>
-  | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >>
-
-let mlexpr_of_binding_kind = function
-  | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >>
-  | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >>
-
-let mlexpr_of_binder_kind = function
-  | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >>
-  | Constrexpr.Generalized (b,b',b'') ->
-      <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$
-	$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
-
-let rec mlexpr_of_constr = function
-  | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
-      anti loc (string_of_id id)
-  | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
-  | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CProdN (loc,l,a) -> <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list
-      (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Constrexpr.CLambdaN (loc,l,a) -> <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CAppExpl (loc,a,l) -> <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Constrexpr.CApp (loc,a,l) -> <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
-  | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CHole (loc, None) -> <:expr< Constrexpr.CHole $dloc$ None >>
-  | Constrexpr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Constrexpr.CNotation(_,ntn,(subst,substl,[])) ->
-      <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$
-              ($mlexpr_of_list mlexpr_of_constr subst$,
-               $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
-  | Constrexpr.CPatVar (loc,n) ->
-      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
-  | _ -> failwith "mlexpr_of_constr: TODO"
-
-let mlexpr_of_occ_constr =
-  mlexpr_of_occurrences mlexpr_of_constr
-
-let mlexpr_of_red_expr = function
-  | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
-  | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
-  | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
-  | Genredexpr.Cbv f ->
-      <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
-  | Genredexpr.Lazy f ->
-      <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >>
-  | Genredexpr.Unfold l ->
-      let f1 = mlexpr_of_by_notation mlexpr_of_reference in
-      let f = mlexpr_of_list (mlexpr_of_occurrences f1) in
-      <:expr< Genredexpr.Unfold $f l$ >>
-  | Genredexpr.Fold l ->
-      <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Genredexpr.Pattern l ->
-      let f = mlexpr_of_list mlexpr_of_occ_constr in
-      <:expr< Genredexpr.Pattern $f l$ >>
-  | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
-  | Genredexpr.ExtraRedExpr s ->
-      <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
-
-let rec mlexpr_of_argtype loc = function
-  | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
-  | Genarg.IntArgType -> <:expr< Genarg.IntArgType >>
-  | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
-  | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
-  | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
-  | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
-  | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
-  | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
-  | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
-  | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
-  | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
-  | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
-  | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
-  | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
-  | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
-  | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
-  | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
-  | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.PairArgType (t1,t2) ->
-      let t1 = mlexpr_of_argtype loc t1 in
-      let t2 = mlexpr_of_argtype loc t2 in
-      <:expr< Genarg.PairArgType $t1$ $t2$ >>
-  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-
-let rec mlexpr_of_may_eval f = function
-  | Genredexpr.ConstrEval (r,c) ->
-      <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
-  | Genredexpr.ConstrContext ((loc,id),c) ->
-      let id = mlexpr_of_ident id in
-      <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >>
-  | Genredexpr.ConstrTypeOf c ->
-      <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >>
-  | Genredexpr.ConstrTerm c ->
-      <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >>
-
-let mlexpr_of_binding_kind = function
-  | Misctypes.ExplicitBindings l ->
-      let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
-      <:expr< Misctypes.ExplicitBindings $l$ >>
-  | Misctypes.ImplicitBindings l ->
-      let l = mlexpr_of_list mlexpr_of_constr l in
-      <:expr< Misctypes.ImplicitBindings $l$ >>
-  | Misctypes.NoBindings ->
-       <:expr< Misctypes.NoBindings >>
-
-let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
-
-let mlexpr_of_constr_with_binding =
-  mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
-
-let mlexpr_of_move_location f = function
-  | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
-  | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
-  | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >>
-  | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >>
-
-let mlexpr_of_induction_arg = function
-  | Tacexpr.ElimOnConstr c ->
-      <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >>
-  | Tacexpr.ElimOnIdent (_,id) ->
-      <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >>
-  | Tacexpr.ElimOnAnonHyp n ->
-      <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >>
-
-let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO"
-
-let mlexpr_of_pattern_ast = mlexpr_of_constr
-
-let mlexpr_of_entry_type = function
-    _ -> failwith "mlexpr_of_entry_type: TODO"
-
-let mlexpr_of_match_pattern = function
-  | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >>
-  | Tacexpr.Subterm (b,ido,t) ->
-      <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
-
-let mlexpr_of_match_context_hyps = function
-  | Tacexpr.Hyp (id,l) ->
-      let f = mlexpr_of_located mlexpr_of_name in
-      <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >>
-  | Tacexpr.Def (id,v,l) ->
-      let f = mlexpr_of_located mlexpr_of_name in
-      <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >>
-
-let mlexpr_of_match_rule f = function
-  | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >>
-  | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >>
-
-let mlexpr_of_message_token = function
-  | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >>
-  | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
-  | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
-
-let mlexpr_of_debug = function
-  | Tacexpr.Off -> <:expr< Tacexpr.Off >>
-  | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
-  | Tacexpr.Info -> <:expr< Tacexpr.Info >>
-
-let rec mlexpr_of_atomic_tactic = function
-  (* Basic tactics *)
-  | Tacexpr.TacIntroPattern pl ->
-      let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
-      <:expr< Tacexpr.TacIntroPattern $pl$ >>
-  | Tacexpr.TacIntrosUntil h ->
-      <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacIntroMove (idopt,idopt') ->
-      let idopt = mlexpr_of_ident_option idopt in
-      let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
-      <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
-  | Tacexpr.TacAssumption ->
-      <:expr< Tacexpr.TacAssumption >>
-  | Tacexpr.TacExact c ->
-      <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
-  | Tacexpr.TacExactNoCheck c ->
-      <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacVmCastNoCheck c ->
-      <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacApply (b,false,cb,None) ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >>
-  | Tacexpr.TacElim (false,cb,cbo) ->
-      let cb = mlexpr_of_constr_with_binding cb in
-      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
-  | Tacexpr.TacElimType c ->
-      <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >>
-  | Tacexpr.TacCase (false,cb) ->
-      let cb = mlexpr_of_constr_with_binding cb in
-      <:expr< Tacexpr.TacCase False $cb$ >>
-  | Tacexpr.TacCaseType c ->
-      <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >>
-  | Tacexpr.TacFix (ido,n) ->
-      let ido = mlexpr_of_ident_option ido in
-      let n = mlexpr_of_int n in
-      <:expr< Tacexpr.TacFix $ido$ $n$ >>
-  | Tacexpr.TacMutualFix (b,id,n,l) ->
-      let b = mlexpr_of_bool b in
-      let id = mlexpr_of_ident id in
-      let n = mlexpr_of_int n in
-      let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
-      let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >>
-  | Tacexpr.TacCofix ido ->
-      let ido = mlexpr_of_ident_option ido in
-      <:expr< Tacexpr.TacCofix $ido$ >>
-  | Tacexpr.TacMutualCofix (b,id,l) ->
-      let b = mlexpr_of_bool b in
-      let id = mlexpr_of_ident id in
-      let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
-      let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >>
-
-  | Tacexpr.TacCut c ->
-      <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
-  | Tacexpr.TacAssert (t,ipat,c) ->
-      let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
-      <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
-	      $mlexpr_of_constr c$ >>
-  | Tacexpr.TacGeneralize cl ->
-      <:expr< Tacexpr.TacGeneralize
-	      $mlexpr_of_list
-                (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >>
-  | Tacexpr.TacGeneralizeDep c ->
-      <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
-  | Tacexpr.TacLetTac (na,c,cl,b) ->
-      let na = mlexpr_of_name na in
-      let cl = mlexpr_of_clause_pattern cl in
-      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$
-	      $mlexpr_of_bool b$ >>
-
-  (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
-      <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$
-                  $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
-      <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
-	$mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple
-	  (mlexpr_of_list mlexpr_of_induction_arg)
-	  (mlexpr_of_option mlexpr_of_constr_with_binding)
-	  (mlexpr_of_pair
-	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))
-	    (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)))))
-	  (mlexpr_of_option mlexpr_of_clause) l$ >>
-
-  (* Context management *)
-  | Tacexpr.TacClear (b,l) ->
-      let l = mlexpr_of_list (mlexpr_of_hyp) l in
-      <:expr< Tacexpr.TacClear $mlexpr_of_bool b$ $l$ >>
-  | Tacexpr.TacClearBody l ->
-      let l = mlexpr_of_list (mlexpr_of_hyp) l in
-      <:expr< Tacexpr.TacClearBody $l$ >>
-  | Tacexpr.TacMove (dep,id1,id2) ->
-      <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$
-              $mlexpr_of_hyp id1$
-              $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
-
-  (* Constructors *)
-  | Tacexpr.TacLeft (ev,l) ->
-      <:expr< Tacexpr.TacLeft $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacRight (ev,l) ->
-      <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacSplit (ev,b,l) ->
-      <:expr< Tacexpr.TacSplit
-        ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>>
-  | Tacexpr.TacAnyConstructor (ev,t) ->
-      <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
-  | Tacexpr.TacConstructor (ev,n,l) ->
-      let n = mlexpr_of_or_var mlexpr_of_int n in
-      <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
-
-  (* Conversion *)
-  | Tacexpr.TacReduce (r,cl) ->
-      let l = mlexpr_of_clause cl in
-      <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
-  | Tacexpr.TacChange (p,c,cl) ->
-      let l = mlexpr_of_clause cl in
-      let g = mlexpr_of_option mlexpr_of_constr in
-      <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >>
-
-  (* Equivalence relations *)
-  | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
-  | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
-  | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
-
-  (* Automation tactics *)
-  | Tacexpr.TacAuto (debug,n,lems,l) ->
-      let d = mlexpr_of_debug debug in
-      let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
-      let lems = mlexpr_of_list mlexpr_of_constr lems in
-      let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
-  | Tacexpr.TacTrivial (debug,lems,l) ->
-      let d = mlexpr_of_debug debug in
-      let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      let lems = mlexpr_of_list mlexpr_of_constr lems in
-      <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
-
-  | _ -> failwith "Quotation of atomic tactic expressions: TODO"
-
-and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
-  | Tacexpr.TacAtom (loc,t) ->
-      <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >>
-  | Tacexpr.TacThen (t1,[||],t2,[||]) ->
-      <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>>
-  | Tacexpr.TacThens (t,tl) ->
-      <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>>
-  | Tacexpr.TacFirst tl ->
-      <:expr< Tacexpr.TacFirst $mlexpr_of_list mlexpr_of_tactic tl$ >>
-  | Tacexpr.TacSolve tl ->
-      <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >>
-  | Tacexpr.TacTry t ->
-      <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacOrelse (t1,t2) ->
-      <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
-  | Tacexpr.TacDo (n,t) ->
-      <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacTimeout (n,t) ->
-      <:expr< Tacexpr.TacTimeout $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacRepeat t ->
-      <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacProgress t ->
-      <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacId l ->
-      <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
-  | Tacexpr.TacFail (n,l) ->
-      <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >>
-(*
-  | Tacexpr.TacInfo t -> TacInfo (loc,f t)
-
-  | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t)))
-  | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t)
-*)
-  | Tacexpr.TacLetIn (isrec,l,t) ->
-      let f =
-	mlexpr_of_pair
-	  (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident)
-	  mlexpr_of_tactic_arg in
-      <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacMatch (lz,t,l) ->
-      <:expr< Tacexpr.TacMatch
-        $mlexpr_of_bool lz$
-        $mlexpr_of_tactic t$
-        $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-  | Tacexpr.TacMatchGoal (lz,lr,l) ->
-      <:expr< Tacexpr.TacMatchGoal
-        $mlexpr_of_bool lz$
-        $mlexpr_of_bool lr$
-        $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-
-  | Tacexpr.TacFun (idol,body) ->
-      <:expr< Tacexpr.TacFun
-        ($mlexpr_of_list mlexpr_of_ident_option idol$,
-         $mlexpr_of_tactic body$) >>
-  | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
-  | Tacexpr.TacArg (_,t) ->
-      <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >>
-  | Tacexpr.TacComplete t ->
-      <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >>
-  | _ -> failwith "Quotation of tactic expressions: TODO"
-
-and mlexpr_of_tactic_arg = function
-  | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id
-  | Tacexpr.MetaIdArg (loc,false,id) ->
-      <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
-  | Tacexpr.TacCall (loc,t,tl) ->
-      <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
-  | Tacexpr.Tacexp t ->
-      <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >>
-  | Tacexpr.ConstrMayEval c ->
-      <:expr< Tacexpr.ConstrMayEval $mlexpr_of_may_eval mlexpr_of_constr c$ >>
-  | Tacexpr.Reference r ->
-      <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >>
-  | _ -> failwith "mlexpr_of_tactic_arg: TODO"
-
-
-IFDEF CAMLP5 THEN
-
-let not_impl x =
-  let desc =
-    if Obj.is_block (Obj.repr x) then
-      "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
-    else "int_val = " ^ string_of_int (Obj.magic x)
-  in
-  failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc)
-
-(* The following function is written without quotation
-   in order to be parsable even by camlp4. The version with
-   quotation can be found in revision <= 12972 of [q_util.ml4] *)
-
-open MLast
-
-let rec patt_of_expr e =
-  let loc = loc_of_expr e in
-  match e with
-    | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2)
-    | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2)
-    | ExLid (_, x) when x = vala "loc" -> PaAny loc
-    | ExLid (_, s) -> PaLid (loc, s)
-    | ExUid (_, s) -> PaUid (loc, s)
-    | ExStr (_, s) -> PaStr (loc, s)
-    | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e)
-    | _ -> not_impl e
-
-let fconstr e =
-  let ee s =
-    mlexpr_of_constr (Pcoq.Gram.entry_parse e
-			(Pcoq.Gram.parsable (Stream.of_string s)))
-  in
-  let ep s = patt_of_expr (ee s) in
-  Quotation.ExAst (ee, ep)
-
-let ftac e =
-  let ee s =
-    mlexpr_of_tactic (Pcoq.Gram.entry_parse e
-			(Pcoq.Gram.parsable (Stream.of_string s)))
-  in
-  let ep s = patt_of_expr (ee s) in
-  Quotation.ExAst (ee, ep)
-
-let _ =
-  Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi);
-  Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi);
-  Quotation.default := "constr"
-
-ELSE
-
-open Pcaml
-
-let expand_constr_quot_expr loc _loc_name_opt contents =
-  mlexpr_of_constr
-    (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents)
-
-let expand_tactic_quot_expr loc _loc_name_opt contents =
-  mlexpr_of_tactic
-    (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents)
-
-let _ =
-  (* FIXME: for the moment, we add quotations in expressions only, not pattern *)
-  Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr;
-  Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr;
-  Quotation.default := "constr"
-
-END
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
deleted file mode 100644
index cfaa2a654..000000000
--- a/parsing/q_util.ml4
+++ /dev/null
@@ -1,69 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* This file defines standard combinators to build ml expressions *)
-
-open Extrawit
-open Compat
-open Pp
-
-let mlexpr_of_list f l =
-  List.fold_right
-    (fun e1 e2 ->
-      let e1 = f e1 in
-       let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
-       <:expr< [$e1$ :: $e2$] >>)
-    l (let loc = dummy_loc in <:expr< [] >>)
-
-let mlexpr_of_pair m1 m2 (a1,a2) =
-  let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
-  <:expr< ($e1$, $e2$) >>
-
-let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
-  let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
-  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
-  <:expr< ($e1$, $e2$, $e3$) >>
-
-let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)=
-  let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in
-  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in
-  <:expr< ($e1$, $e2$, $e3$, $e4$) >>
-
-(* We don't give location for tactic quotation! *)
-let loc = dummy_loc
-
-
-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$ >>
-
-open Vernacexpr
-open Genarg
-
-let rec mlexpr_of_prod_entry_key = function
-  | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Aself -> <:expr< Pcoq.Aself >>
-  | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
-  | Pcoq.Agram s -> Errors.anomaly "Agram not supported"
-  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >>
-  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
deleted file mode 100644
index 5d56c456f..000000000
--- a/parsing/q_util.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Compat
-
-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_triple :
-  ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr)
-    -> 'a * 'b * 'c -> MLast.expr
-
-val mlexpr_of_quadruple :
-  ('a -> MLast.expr) -> ('b -> MLast.expr) ->
-    ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> 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_prod_entry_key : Pcoq.prod_entry_key -> MLast.expr
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
deleted file mode 100644
index ec0784c52..000000000
--- a/parsing/tacextend.ml4
+++ /dev/null
@@ -1,235 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
-open Util
-open Pp
-open Genarg
-open Q_util
-open Q_coqast
-open Argextend
-open Pcoq
-open Extrawit
-open Egramml
-open Compat
-
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | GramNonTerminal(loc',_,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_when loc = function
-  | [] -> <:expr< True >>
-  | GramNonTerminal(loc',t,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      let l = make_when loc l in
-      let loc = join_loc loc' loc in
-      let t = mlexpr_of_argtype loc' t in
-      <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
-  | _::l -> make_when loc l
-
-let rec make_let e = function
-  | [] -> e
-  | GramNonTerminal(loc,t,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      let loc = join_loc loc (MLast.loc_of_expr e) in
-      let e = make_let e l in
-      let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
-      <:expr< let $lid:p$ = $v$ in $e$ >>
-  | _::l -> make_let e l
-
-let rec extract_signature = function
-  | [] -> []
-  | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
-  | _::l -> extract_signature l
-
-let check_unicity s l =
-  let l' = List.map (fun (l,_) -> extract_signature l) l in
-  if not (Util.list_distinct l') then
-    Pp.warning_with !Pp_control.err_ft
-      ("Two distinct rules of tactic entry "^s^" have the same\n"^
-      "non-terminals in the same order: put them in distinct tactic entries")
-
-let make_clause (pt,e) =
-  (make_patt pt,
-   vala (Some (make_when (MLast.loc_of_expr e) pt)),
-   make_let e pt)
-
-let make_fun_clauses loc s l =
-  check_unicity s l;
-  Compat.make_fun loc (List.map make_clause l)
-
-let rec make_args = function
-  | [] -> <:expr< [] >>
-  | GramNonTerminal(loc,t,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
-  | _::l -> make_args l
-
-let rec make_eval_tactic e = function
-  | [] -> e
-  | GramNonTerminal(loc,tag,_,Some p)::l when is_tactic_genarg tag ->
-      let p = Names.string_of_id p in
-      let loc = join_loc loc (MLast.loc_of_expr e) in
-      let e = make_eval_tactic e l in
-      <:expr< let $lid:p$ = $lid:p$ in $e$ >>
-  | _::l -> make_eval_tactic e l
-
-let rec make_fun e = function
-  | [] -> e
-  | GramNonTerminal(loc,_,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      <:expr< fun $lid:p$ -> $make_fun e l$ >>
-  | _::l -> make_fun e l
-
-let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
-  | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
-  | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >>
-
-let make_prod_item = function
-  | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | GramNonTerminal (loc,nt,g,sopt) ->
-      <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
-      $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
-
-let mlexpr_of_clause =
-  mlexpr_of_list (fun (a,b) -> mlexpr_of_list make_prod_item a)
-
-let rec make_tags loc = function
-  | [] -> <:expr< [] >>
-  | GramNonTerminal(loc',t,_,Some p)::l ->
-      let l = make_tags loc l in
-      let loc = join_loc loc' loc in
-      let t = mlexpr_of_argtype loc' t in
-      <:expr< [ $t$ :: $l$ ] >>
-  | _::l -> make_tags loc l
-
-let make_one_printing_rule se (pt,e) =
-  let level = mlexpr_of_int 0 in (* only level 0 supported here *)
-  let loc = MLast.loc_of_expr e in
-  let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
-  <:expr< ($se$, $make_tags loc pt$, ($level$, $prods$)) >>
-
-let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
-
-let rec possibly_empty_subentries loc = function
-  | [] -> []
-  | (s,prodsl) :: l ->
-    let rec aux = function
-    | [] -> (false,<:expr< None >>)
-    | prods :: rest ->
-      try
-        let l = List.map (function
-        | GramNonTerminal(_,(List0ArgType _|
-                             OptArgType _|
-                             ExtraArgType _ as t),_,_)->
-            (* This possibly parses epsilon *)
-            let rawwit = make_rawwit loc t in
-            <:expr< match Genarg.default_empty_value $rawwit$ with
-                    [ None -> failwith ""
-                    | Some v ->
-                        Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign
-                          (Genarg.in_gen $rawwit$ v) ] >>
-        | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
-            (* This does not parse epsilon (this Exit is static time) *)
-             raise Exit) prods in
-        if has_extraarg prods then
-          (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$
-                        with [ Failure "" -> $snd (aux rest)$ ] >>)
-        else
-          (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>)
-      with Exit -> aux rest in
-    let (nonempty,v) = aux prodsl in
-    if nonempty then (s,v) :: possibly_empty_subentries loc l
-    else possibly_empty_subentries loc l
-
-let possibly_atomic loc prods =
-  let l = list_map_filter (function
-    | GramTerminal s :: l, _ -> Some (s,l)
-    | _ -> None) prods in
-  possibly_empty_subentries loc (list_factorize_left l)
-
-let declare_tactic loc s cl =
-  let se = mlexpr_of_string s in
-  let pp = make_printing_rule se cl in
-  let gl = mlexpr_of_clause cl in
-  let hide_tac (p,e) =
-    (* reste a definir les fonctions cachees avec des noms frais *)
-    let stac = "h_"^s in
-    let e =
-      make_fun
-        <:expr<
-          Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$
-        >>
-      p in
-    <:str_item< value $lid:stac$ = $e$ >>
-  in
-  let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
-  let atomic_tactics =
-    mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
-      (possibly_atomic loc cl) in
-  declare_str_items loc
-   (hidden @
-    [ <:str_item< do {
-      try
-        let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
-        List.iter
-          (fun (s,l) -> match l with
-           [ Some l ->
-              Tacinterp.add_primitive_tactic s
-              (Tacexpr.TacAtom($default_loc$,
-                 Tacexpr.TacExtend($default_loc$,$se$,l)))
-           | None -> () ])
-          $atomic_tactics$
-      with e -> Pp.pp (Errors.print e);
-      Egramml.extend_tactic_grammar $se$ $gl$;
-      List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
-    ])
-
-open Pcaml
-open PcamlSig
-
-EXTEND
-  GLOBAL: str_item;
-  str_item:
-    [ [ "TACTIC"; "EXTEND"; s = tac_name;
-        OPT "|"; l = LIST1 tacrule SEP "|";
-        "END" ->
-         declare_tactic loc s l ] ]
-  ;
-  tacrule:
-    [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
-        ->
-	  if match List.hd l with GramNonTerminal _ -> true | _ -> false then
-	    (* En attendant la syntaxe de tacticielles *)
-	    failwith "Tactic syntax must start with an identifier";
-	  (l,e)
-    ] ]
-  ;
-  tacargs:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
-        GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
-        GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | s = STRING ->
-	if s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal.");
-        GramTerminal s
-    ] ]
-  ;
-  tac_name:
-    [ [ s = LIDENT -> s
-      | s = UIDENT -> s
-    ] ]
-  ;
-  END
-
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
deleted file mode 100644
index 94135d121..000000000
--- a/parsing/vernacextend.ml4
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "tools/compat5b.cmo" i*)
-
-open Pp
-open Util
-open Genarg
-open Q_util
-open Q_coqast
-open Argextend
-open Tacextend
-open Pcoq
-open Egramml
-open Compat
-
-let rec make_let e = function
-  | [] -> e
-  | GramNonTerminal(loc,t,_,Some p)::l ->
-      let p = Names.string_of_id p in
-      let loc = join_loc 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 check_unicity s l =
-  let l' = List.map (fun (_,l,_) -> extract_signature l) l in
-  if not (Util.list_distinct l') then
-    Pp.warning_with !Pp_control.err_ft
-      ("Two distinct rules of entry "^s^" have the same\n"^
-      "non-terminals in the same order: put them in distinct vernac entries")
-
-let make_clause (_,pt,e) =
-  (make_patt pt,
-   vala (Some (make_when (MLast.loc_of_expr e) pt)),
-   make_let e pt)
-
-let make_fun_clauses loc s l =
-  check_unicity s l;
-  Compat.make_fun loc (List.map make_clause l)
-
-let mlexpr_of_clause =
-  mlexpr_of_list
-    (fun (a,b,c) -> mlexpr_of_list make_prod_item 
-       (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b))
-
-let declare_command loc s nt cl =
-  let gl = mlexpr_of_clause cl in
-  let funcl = make_fun_clauses loc s cl in
-  declare_str_items loc
-    [ <:str_item< do {
-	try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$
-	with e -> Pp.pp (Errors.print e);
-	Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$
-      } >> ]
-
-open Pcaml
-open PcamlSig
-
-EXTEND
-  GLOBAL: str_item;
-  str_item:
-    [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT;
-        OPT "|"; l = LIST1 rule SEP "|";
-        "END" ->
-         declare_command loc s <:expr<None>> l 
-      | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT;
-        OPT "|"; l = LIST1 rule SEP "|";
-        "END" ->
-          declare_command loc s <:expr<Some $lid:nt$>> l ] ]
-  ;
-  (* 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; "]"; "->"; "["; e = Pcaml.expr; "]"
-        ->
-      if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty.");
-      (Some s,l,<:expr< fun () -> $e$ >>)
-      | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
-	  (None,l,<:expr< fun () -> $e$ >>)
-    ] ]
-  ;
-  args:
-    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
-        GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
-        GramNonTerminal (loc, t, g, Some (Names.id_of_string s))
-      | s = STRING ->
-        GramTerminal s
-    ] ]
-  ;
-  END
-;;