Imported Upstream version 8.5~beta1+dfsg

8 files changed, 1622 insertions, 0 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
new file mode 100644
index 00000000..fe0959dd
--- /dev/null
+++ b/grammar/argextend.ml4
@@ -0,0 +1,299 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 Compat
+open Pcoq
+
+let loc = CompatLoc.ghost
+let default_loc = <:expr< Loc.ghost >>
+
+let qualified_name loc s =
+  let path = CString.split '.' s in
+  let (name, path) = CList.sep_last path in
+  qualified_name loc path name
+
+let mk_extraarg loc s =
+  try
+    let name = Genarg.get_name0 s in
+    qualified_name loc name
+  with Not_found ->
+    <:expr< $lid:"wit_"^s$ >>
+
+let rec make_wit loc = function
+  | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
+  | IdentArgType -> <:expr< Constrarg.wit_ident >>
+  | VarArgType -> <:expr< Constrarg.wit_var >>
+  | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
+  | GenArgType -> <:expr< Constrarg.wit_genarg >>
+  | ConstrArgType -> <:expr< Constrarg.wit_constr >>
+  | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
+  | RedExprArgType -> <:expr< Constrarg.wit_red_expr >>
+  | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
+  | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >>
+  | BindingsArgType -> <:expr< Constrarg.wit_bindings >>
+  | 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 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 has_extraarg =
+  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+
+let rec is_possibly_empty = function
+| Aopt _ | Alist0 _ | Alist0sep _ | Amodifiers _ -> true
+| Alist1 t | Alist1sep (t, _) -> is_possibly_empty t
+| _ -> false
+
+let rec get_empty_entry = function
+| Aopt _ -> <:expr< None >>
+| Alist0 _ | Alist0sep _ | Amodifiers _ -> <:expr< [] >>
+| Alist1 t | Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
+| _ -> assert 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(_,_,e,_) ->
+        is_possibly_empty e
+    | GramTerminal _ ->
+        (* 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.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+  let rec aux = function
+    | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
+    | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e ->
+        bind_name p (get_empty_entry e) (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.Id.to_string id in
+        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit 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 [ Exit -> 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.Id.to_string 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 ->
+      begin match rawtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun ist v -> (ist, v) >>
+      | _ ->
+        <:expr< fun ist v ->
+          let ans = out_gen $make_globwit loc rawtyp$
+          (Tacintern.intern_genarg ist
+          (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
+          (ist, ans) >>
+      end
+    | Some f ->
+      <:expr< fun ist v -> (ist, $lid:f$ ist v) >>
+  in
+  let interp = match f with
+    | None ->
+      begin match globtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun ist gl v -> (gl.Evd.sigma, v) >>
+      | _ ->
+	<:expr< fun ist gl x ->
+	  let (sigma,a_interp) =
+	    Tacinterp.interp_genarg ist
+              (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it
+               (Genarg.in_gen $make_globwit loc globtyp$ x)
+	  in
+          (sigma , out_gen $make_topwit loc globtyp$ a_interp)>>
+      end
+    | Some f -> <:expr< $lid:f$>> in
+  let subst = match h with
+    | None ->
+      begin match globtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun s v -> v >>
+      | _ ->
+        <:expr< fun s x ->
+          out_gen $make_globwit loc globtyp$
+          (Tacsubst.subst_genarg s
+            (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+      end
+    | Some f -> <:expr< $lid:f$>> in
+  let se = mlexpr_of_string s in
+  let wit = <:expr< $lid:"wit_"^s$ >> in
+  let rawwit = <:expr< Genarg.rawwit $wit$ >> 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$) = Genarg.make0 $default_value$ $se$ >>;
+     <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
+     <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
+     <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
+     <: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
+        $wit$ $lid:rawpr$ $lid:globpr$ $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< Genarg.rawwit $wit$ >> 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.genarg_type 'a unit unit) =
+        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 $wit$
+        $pr_rules$
+        (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer"))
+        (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
+      >> ]
+
+open Pcoq
+open Pcaml
+open PcamlSig (* necessary for camlp4 *)
+
+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" -> ListArgType 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/grammar/grammar.mllib b/grammar/grammar.mllib
new file mode 100644
index 00000000..0b168377
--- /dev/null
+++ b/grammar/grammar.mllib
@@ -0,0 +1,62 @@
+Coq_config
+
+Hook
+Canary
+Hashset
+Hashcons
+CSet
+CMap
+Int
+HMap
+Option
+Store
+Exninfo
+Backtrace
+Pp_control
+Flags
+Loc
+Serialize
+Stateid
+Feedback
+Pp
+Errors
+CList
+CString
+CArray
+CStack
+Util
+Bigint
+Predicate
+Segmenttree
+Unicodetable
+Unicode
+Genarg
+
+Evar
+Names
+
+Libnames
+
+Redops
+Miscops
+Locusops
+
+Stdarg
+Constrarg
+Constrexpr_ops
+
+Compat
+Tok
+Lexer
+Pcoq
+G_prim
+G_tactic
+G_ltac
+G_constr
+
+Q_util
+Q_coqast
+Egramml
+Argextend
+Tacextend
+Vernacextend
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
new file mode 100644
index 00000000..6ae8bea3
--- /dev/null
+++ b/grammar/q_constr.ml4
@@ -0,0 +1,120 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 Q_util
+open Compat
+open Pcaml
+open PcamlSig (* necessary for camlp4 *)
+
+let loc = CompatLoc.ghost
+let dloc = <:expr< Loc.ghost >>
+
+let apply_ref f l =
+  <:expr<
+    Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$)
+  >>
+
+EXTEND
+  GLOBAL: expr;
+  expr:
+    [ [ "PATTERN"; "["; c = constr; "]" ->
+      <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
+  ;
+  sort:
+    [ [ "Set"  -> Misctypes.GSet
+      | "Prop" -> Misctypes.GProp
+      | "Type" -> Misctypes.GType [] ] ]
+  ;
+  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),Misctypes.IntroAnonymous,None) >>
+      | "?"; 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$, None) >>
+      | 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/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
new file mode 100644
index 00000000..dd97107f
--- /dev/null
+++ b/grammar/q_coqast.ml4
@@ -0,0 +1,597 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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 = CompatLoc.ghost
+
+let dloc = <:expr< Loc.ghost >>
+
+let mlexpr_of_ident id =
+  <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >>
+
+let mlexpr_of_name = function
+  | Names.Anonymous -> <:expr< Names.Anonymous >>
+  | Names.Name id ->
+      <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >>
+
+let mlexpr_of_dirpath dir =
+  let l = Names.DirPath.repr dir in
+  <:expr< Names.DirPath.make $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) ->
+    let loc = of_coqloc loc in <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
+  | Libnames.Ident (loc,id) ->
+    let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
+
+let mlexpr_of_union f g = function
+  | Util.Inl a -> <:expr< Util.Inl $f a$ >>
+  | Util.Inr b -> <:expr< Util.Inr $g b$ >>
+
+let mlexpr_of_located f (loc,x) =
+  let loc = of_coqloc loc in
+  <: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) ->
+      let loc = of_coqloc loc in
+      <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
+
+let mlexpr_of_global_flag = function
+  | Tacexpr.TacGlobal -> <:expr<Tacexpr.TacGlobal>>
+  | Tacexpr.TacLocal  -> <:expr<Tacexpr.TacLocal>>
+
+let mlexpr_of_intro_pattern_disjunctive = function
+  _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO"
+
+let mlexpr_of_intro_pattern_naming = function
+  | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
+  | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
+  | Misctypes.IntroIdentifier id ->
+      <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
+
+let mlexpr_of_intro_pattern = function
+  | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
+  | Misctypes.IntroNaming pat ->
+      <:expr< Misctypes.IntroNaming $mlexpr_of_intro_pattern_naming pat$ >>
+  | Misctypes.IntroAction _ ->
+      failwith "mlexpr_of_intro_pattern: TODO"
+
+let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
+
+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_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_instance c = <:expr< None >>
+
+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 (Id.to_string id) ->
+      let loc = of_coqloc loc in
+      anti loc (Id.to_string id)
+  | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >>
+  | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Constrexpr.CProdN (loc,l,a) ->
+      let loc = of_coqloc loc in
+      <: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) ->
+    let loc = of_coqloc loc in
+    <: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,(p,r,us),l) ->
+    let loc = of_coqloc loc in
+    let a = (p,r,us) in
+    <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_triple (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference mlexpr_of_instance a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Constrexpr.CApp (loc,a,l) ->
+    let loc = of_coqloc loc in
+    <: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, ipat, None) ->
+    let loc = of_coqloc loc in
+    <:expr< Constrexpr.CHole $dloc$ None $mlexpr_of_intro_pattern_naming ipat$ None >>
+  | Constrexpr.CHole (loc,_,_,_) -> 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) ->
+      let loc = of_coqloc loc in
+      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_ident n$ >>
+  | Constrexpr.CEvar (loc,n,[]) ->
+      let loc = of_coqloc loc in
+      <:expr< Constrexpr.CEvar $dloc$ $mlexpr_of_ident n$ [] >>
+  | _ -> failwith "mlexpr_of_constr: TODO"
+
+let mlexpr_of_occ_constr =
+  mlexpr_of_occurrences mlexpr_of_constr
+
+let mlexpr_of_occ_ref_or_constr =
+  mlexpr_of_occurrences
+    (mlexpr_of_union
+       (mlexpr_of_by_notation mlexpr_of_reference) 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 (f,o) ->
+      <:expr< Genredexpr.Simpl $mlexpr_of_red_flags f$ $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
+  | Genredexpr.Cbv f ->
+      <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
+  | Genredexpr.Cbn f ->
+      <:expr< Genredexpr.Cbn $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_ref_or_constr o$ >>
+  | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
+  | Genredexpr.ExtraRedExpr s ->
+      <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
+
+let rec mlexpr_of_argtype loc = function
+  | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
+  | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
+  | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
+  | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
+  | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
+  | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
+  | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
+  | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
+  | Genarg.GenArgType -> <:expr< Genarg.GenArgType >>
+  | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
+  | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
+  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $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 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 loc = of_coqloc loc in
+      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_constr_with_binding_arg =
+  mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding
+
+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_lazy_flag = function
+  | Tacexpr.General -> <:expr<Tacexpr.General>>
+  | Tacexpr.Select    -> <:expr<Tacexpr.Select>>
+  | Tacexpr.Once    -> <:expr<Tacexpr.Once>>
+
+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.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.TacExact c ->
+      <:expr< Tacexpr.TacExact $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_arg cb$ None >>
+  | Tacexpr.TacElim (false,cb,cbo) ->
+      let cb = mlexpr_of_constr_with_binding_arg cb in
+      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
+      <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
+  | Tacexpr.TacCase (false,cb) ->
+      let cb = mlexpr_of_constr_with_binding_arg cb in
+      <:expr< Tacexpr.TacCase False $cb$ >>
+  | 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 (id,n,l) ->
+      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 $id$ $n$ $l$ >>
+  | Tacexpr.TacCofix ido ->
+      let ido = mlexpr_of_ident_option ido in
+      <:expr< Tacexpr.TacCofix $ido$ >>
+  | Tacexpr.TacMutualCofix (id,l) ->
+      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 $id$ $l$ >>
+
+  | Tacexpr.TacAssert (b,t,ipat,c) ->
+      let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
+      <:expr< Tacexpr.TacAssert $mlexpr_of_bool b$
+              $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,e) ->
+      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$
+	      (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e)
+      >>
+
+  (* Derived basic tactics *)
+  | 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_pair
+                 (mlexpr_of_option mlexpr_of_bool)
+                 mlexpr_of_induction_arg)
+	      (mlexpr_of_pair
+		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern_naming))
+		 (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive)))
+	      (mlexpr_of_option mlexpr_of_clause)))
+	(mlexpr_of_option mlexpr_of_constr_with_binding)
+ 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 (id1,id2) ->
+      <:expr< Tacexpr.TacMove
+              $mlexpr_of_hyp id1$
+              $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
+
+  (* Constructors *)
+  | Tacexpr.TacSplit (ev,l) ->
+      <:expr< Tacexpr.TacSplit
+        ($mlexpr_of_bool ev$, $mlexpr_of_list 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.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
+
+  (* 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) ->
+      let loc = of_coqloc loc in
+      <: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.TacOr (t1,t2) ->
+      <:expr< Tacexpr.TacOr $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
+  | 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.TacShowHyps t ->
+      <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
+  | Tacexpr.TacId l ->
+      <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
+  | Tacexpr.TacFail (g,n,l) ->
+      <:expr< Tacexpr.TacFail $mlexpr_of_global_flag g$ $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_match_lazy_flag 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_match_lazy_flag 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) ->
+    let loc = of_coqloc loc in
+    anti loc id
+  | Tacexpr.MetaIdArg (loc,false,id) ->
+    let loc = of_coqloc loc in
+    <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
+  | Tacexpr.TacCall (loc,t,tl) ->
+    let loc = of_coqloc loc in
+    <: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/grammar/q_util.ml4 b/grammar/q_util.ml4
new file mode 100644
index 00000000..18b1ccd3
--- /dev/null
+++ b/grammar/q_util.ml4
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 Compat
+
+let mlexpr_of_list f l =
+  List.fold_right
+    (fun e1 e2 ->
+      let e1 = f e1 in
+       let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+       <:expr< [$e1$ :: $e2$] >>)
+    l (let loc = CompatLoc.ghost in <:expr< [] >>)
+
+let mlexpr_of_pair m1 m2 (a1,a2) =
+  let e1 = m1 a1 and e2 = m2 a2 in
+  let loc = CompatLoc.merge (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 = CompatLoc.merge (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 = CompatLoc.merge (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 = CompatLoc.ghost
+
+
+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 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 (Pp.str "Agram not supported")
+  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >>
+  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
new file mode 100644
index 00000000..7393a0d5
--- /dev/null
+++ b/grammar/q_util.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Compat (* necessary for camlp4 *)
+
+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/grammar/tacextend.ml4 b/grammar/tacextend.ml4
new file mode 100644
index 00000000..0421ad7c
--- /dev/null
+++ b/grammar/tacextend.ml4
@@ -0,0 +1,281 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 Names
+open Genarg
+open Q_util
+open Q_coqast
+open Argextend
+open Pcoq
+open Egramml
+open Compat
+
+let dloc = <:expr< Loc.ghost >>
+
+let plugin_name = <:expr< __coq_plugin_name >>
+
+let rec make_patt = function
+  | [] -> <:patt< [] >>
+  | GramNonTerminal(loc',_,_,Some p)::l ->
+      let p = Names.Id.to_string 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 loc' = of_coqloc loc' in
+      let p = Names.Id.to_string p in
+      let l = make_when loc l in
+      let loc = CompatLoc.merge loc' loc in
+      let t = mlexpr_of_argtype loc' t in
+      <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
+  | _::l -> make_when loc l
+
+let rec make_let raw e = function
+  | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
+  | GramNonTerminal(loc,t,_,Some p)::l ->
+      let loc = of_coqloc loc in
+      let p = Names.Id.to_string p in
+      let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
+      let e = make_let raw e l in
+      let v =
+        if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
+               else <:expr< Genarg.out_gen $make_topwit    loc t$ $lid:p$ >> in
+      <:expr< let $lid:p$ = $v$ in $e$ >>
+  | _::l -> make_let raw 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.msg_warning
+      (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
+      "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 false 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 loc = of_coqloc loc in
+      let p = Names.Id.to_string p in
+      <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
+  | _::l -> make_args l
+
+let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
+  | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
+  | GramNonTerminal (loc,nt,_,sopt) ->
+    let loc = of_coqloc loc in <:expr< None >>
+
+let make_prod_item = function
+  | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | GramNonTerminal (loc,nt,g,sopt) ->
+      let loc = of_coqloc loc in
+      <: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 loc' = of_coqloc loc' in
+      let l = make_tags loc l in
+      let loc = CompatLoc.merge 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$, { Pptactic.pptac_args = $make_tags loc pt$;
+            pptac_prods = ($level$, $prods$) }) >>
+
+let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
+
+let make_empty_check = function
+| GramNonTerminal(_, t, e, _)->
+  let is_extra = match t with ExtraArgType _ -> true | _ -> false in
+  if is_possibly_empty e || is_extra then
+    (* This possibly parses epsilon *)
+    let wit = make_wit loc t in
+    let rawwit = make_rawwit loc t in
+    <:expr<
+      match Genarg.default_empty_value $wit$ with
+      [ None -> raise Exit
+      | Some v ->
+        Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
+          (Genarg.in_gen $rawwit$ v) ] >>
+  else
+  (* This does not parse epsilon (this Exit is static time) *)
+    raise Exit
+| GramTerminal _ ->
+  (* Idem *)
+  raise Exit
+
+let rec possibly_empty_subentries loc = function
+  | [] -> []
+  | (s,prodsl) :: l ->
+    let rec aux = function
+    | [] -> (false,<:expr< None >>)
+    | prods :: rest ->
+      try
+        let l = List.map make_empty_check prods in
+        if has_extraarg prods then
+          (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$
+                        with [ Exit -> $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 String.equal l)
+
+(** Special treatment of constr entries *)
+let is_constr_gram = function
+| GramTerminal _ -> false
+| GramNonTerminal (_, _, e, _) ->
+  match e with
+  | Aentry ("constr", "constr") -> true
+  | _ -> false
+
+let make_vars len =
+  (** We choose names unlikely to be written by a human, even though that
+      does not matter at all. *)
+  List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i)))
+
+let declare_tactic loc s c cl = match cl with
+| [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
+  (** The extension is only made of a name followed by constr entries: we do not
+      add any grammar nor printing rule and add it as a true Ltac definition. *)
+  let patt = make_patt rem in
+  let vars = make_vars (List.length rem) in
+  let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
+  let entry = mlexpr_of_string s in
+  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
+  let name = mlexpr_of_string name in
+  let tac =
+    (** Special handling of tactics without arguments: such tactics do not do
+        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
+        whole-prof tactics like [shelve_unifiable]. *)
+    if List.is_empty rem then
+      <:expr< fun _ $lid:"ist"$ -> $tac$ >>
+    else
+      let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+      <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
+  in
+  (** Arguments are not passed directly to the ML tactic in the TacML node,
+      the ML tactic retrieves its arguments in the [ist] environment instead.
+      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $se$, [])) >> in
+  let name = <:expr< Names.Id.of_string $name$ >> in
+  declare_str_items loc
+    [ <:str_item< do {
+      let obj () = Tacenv.register_ltac True False $name$ $body$ in
+      try do {
+        Tacenv.register_ml_tactic $se$ $tac$;
+        Mltop.declare_cache_obj obj $plugin_name$; }
+      with [ e when Errors.noncritical e ->
+        Pp.msg_warning
+          (Pp.app
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+            (Errors.print e)) ]; } >>
+    ]
+| _ ->
+  (** Otherwise we add parsing and printing rules to generate a call to a
+      TacML tactic. *)
+  let entry = mlexpr_of_string s in
+  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
+  let pp = make_printing_rule se cl in
+  let gl = mlexpr_of_clause cl in
+  let atom =
+    mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
+      (possibly_atomic loc cl) in
+  let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$ >> in
+  declare_str_items loc
+    [ <:str_item< do {
+      try do {
+        Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
+        Mltop.declare_cache_obj $obj$ $plugin_name$;
+        List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
+      with [ e when Errors.noncritical e ->
+        Pp.msg_warning
+          (Pp.app
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+            (Errors.print e)) ]; } >>
+    ]
+
+open Pcaml
+open PcamlSig (* necessary for camlp4 *)
+
+EXTEND
+  GLOBAL: str_item;
+  str_item:
+    [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
+        OPT "|"; l = LIST1 tacrule SEP "|";
+        "END" ->
+         declare_tactic loc s c l ] ]
+  ;
+  tacrule:
+    [ [ "["; l = LIST1 tacargs; "]";
+        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
+        "->"; "["; e = Pcaml.expr; "]" ->
+	(match l with
+	  | GramNonTerminal _ :: _ ->
+	    (* En attendant la syntaxe de tacticielles *)
+	    failwith "Tactic syntax must start with an identifier"
+	  | _ -> (l,c,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 String.is_empty 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/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
new file mode 100644
index 00000000..7a4d52ab
--- /dev/null
+++ b/grammar/vernacextend.ml4
@@ -0,0 +1,166 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 Q_util
+open Argextend
+open Tacextend
+open Pcoq
+open Egramml
+open Compat
+
+let rec make_let e = function
+  | [] -> e
+  | GramNonTerminal(loc,t,_,Some p)::l ->
+      let loc = of_coqloc loc in
+      let p = Names.Id.to_string p in
+      let loc = CompatLoc.merge 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 (_,pt,_,e) =
+  (make_patt pt,
+   vala (Some (make_when (MLast.loc_of_expr e) pt)),
+   make_let e pt)
+
+(* To avoid warnings *)
+let mk_ignore c pt =
+  let names = CList.map_filter (function
+  | GramNonTerminal(_,_,_,Some p) -> Some (Names.Id.to_string p)
+  | _ -> None) 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 (_,pt,c,_) =
+  match c ,cg with
+  | Some c, _ ->
+     (make_patt pt,
+      vala (Some (make_when (MLast.loc_of_expr c) pt)),
+      make_let (mk_ignore c pt) pt)
+  | None, Some cg ->
+     (make_patt pt,
+      vala (Some (make_when (MLast.loc_of_expr cg) pt)),
+      <:expr< fun () -> $cg$ $str:s$ >>)
+  | None, None -> msg_warning
+      (strbrk("Vernac entry \""^s^"\" misses a classifier. "^
+         "A classifier is a function that returns an expression "^
+         "of type vernac_classification (see Vernacexpr). You can: ")++
+       str"- "++hov 0 (
+        strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
+          "new vernacular command does not alter the system state;"))++fnl()++
+       str"- "++hov 0 (
+        strbrk("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;"))++fnl()++
+       str"- "++hov 0 (
+        strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
+          "a global function f.  The function f will be called passing "^
+          "\""^s^"\" as the only argument;")) ++fnl()++
+       str"- "++hov 0 (
+        strbrk"Add a specific classifier in each clause using the syntax:"
+        ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++
+       strbrk("Specific classifiers have precedence over global "^
+         "classifiers. Only one classifier is called.")++fnl());
+    (make_patt pt,
+      vala (Some (make_when loc pt)),
+      <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
+
+let make_fun_clauses loc s l =
+  let cl = List.map (fun c -> Compat.make_fun loc [make_clause c]) l in
+  mlexpr_of_list (fun x -> x) cl
+
+let make_fun_classifiers loc s c l =
+  let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
+  mlexpr_of_list (fun x -> x) cl
+
+let mlexpr_of_clause =
+  mlexpr_of_list
+    (fun (a,b,_,_) -> mlexpr_of_list make_prod_item
+       (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b))
+
+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
+  declare_str_items loc
+    [ <:str_item< do {
+	try do {
+          CList.iteri (fun i f -> Vernacinterp.vinterp_add ($se$, i) f) $funcl$;
+          CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ }
+	with [ e when Errors.noncritical e ->
+	  Pp.msg_warning
+	    (Pp.app
+	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
+	       (Errors.print e)) ];
+	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
+      } >> ]
+
+open Pcaml
+open PcamlSig (* necessary for camlp4 *)
+
+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"; 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 $str: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 >>
+    ] ]
+  ;
+  (* 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; "]";
+        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ];
+                  "->"; "["; e = Pcaml.expr; "]" ->
+      if String.is_empty s then
+        Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+      (Some s,l,c,<:expr< fun () -> $e$ >>)
+      | "[" ; "-" ; l = LIST1 args ; "]" ;
+        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ];
+                  "->"; "["; e = Pcaml.expr; "]" ->
+      (None,l,c,<: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
+;;