Port to coqpp.

4 files changed, 939 insertions, 871 deletions

diff --git a/_CoqProject b/_CoqProject
index 15e02a6484..071066dd86 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,7 +30,7 @@ src/tac2tactics.ml
 src/tac2tactics.mli
 src/tac2stdlib.ml
 src/tac2stdlib.mli
-src/g_ltac2.ml4
+src/g_ltac2.mlg
 src/ltac2_plugin.mlpack
 
 theories/Init.v
diff --git a/src/dune b/src/dune
index b0140aa809..7c911fb041 100644
--- a/src/dune
+++ b/src/dune
@@ -6,5 +6,5 @@
 
 (rule
  (targets g_ltac2.ml)
- (deps (:pp-file g_ltac2.ml4) )
- (action (run coqp5 -loc loc -impl %{pp-file} -o %{targets})))
+ (deps (:mlg-file g_ltac2.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
deleted file mode 100644
index cb42b393db..0000000000
--- a/src/g_ltac2.ml4
+++ /dev/null
@@ -1,868 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-open Tok
-open Pcoq
-open Constrexpr
-open Tac2expr
-open Tac2qexpr
-open Ltac_plugin
-
-let err () = raise Stream.Failure
-
-type lookahead = int -> Tok.t Stream.t -> int option
-
-let entry_of_lookahead s (lk : lookahead) =
-  let run strm = match lk 0 strm with None -> err () | Some _ -> () in
-  Gram.Entry.of_parser s run
-
-let (>>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
-| None -> None
-| Some n -> lk2 n strm
-
-let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
-| None -> lk2 n strm
-| Some n -> Some n
-
-let lk_kw kw n strm = match stream_nth n strm with
-| KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
-| _ -> None
-
-let lk_ident n strm = match stream_nth n strm with
-| IDENT _ -> Some (n + 1)
-| _ -> None
-
-let lk_int n strm = match stream_nth n strm with
-| INT _ -> Some (n + 1)
-| _ -> None
-
-let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident)
-
-(* lookahead for (x:=t), (?x:=t) and (1:=t) *)
-let test_lpar_idnum_coloneq =
-  entry_of_lookahead "test_lpar_idnum_coloneq" begin
-    lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":="
-  end
-
-(* lookahead for (x:t), (?x:t) *)
-let test_lpar_id_colon =
-  entry_of_lookahead "test_lpar_id_colon" begin
-    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
-  end
-
-(* Hack to recognize "(x := t)" and "($x := t)" *)
-let test_lpar_id_coloneq =
-  entry_of_lookahead "test_lpar_id_coloneq" begin
-    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
-  end
-
-(* Hack to recognize "(x)" *)
-let test_lpar_id_rpar =
-  entry_of_lookahead "test_lpar_id_rpar" begin
-    lk_kw "(" >> lk_ident >> lk_kw ")"
-  end
-
-let test_ampersand_ident =
-  entry_of_lookahead "test_ampersand_ident" begin
-    lk_kw "&" >> lk_ident
-  end
-
-let test_dollar_ident =
-  entry_of_lookahead "test_dollar_ident" begin
-    lk_kw "$" >> lk_ident
-  end
-
-let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Entry.create "tactic:tac2type"
-let tac2def_val = Entry.create "tactic:tac2def_val"
-let tac2def_typ = Entry.create "tactic:tac2def_typ"
-let tac2def_ext = Entry.create "tactic:tac2def_ext"
-let tac2def_syn = Entry.create "tactic:tac2def_syn"
-let tac2def_mut = Entry.create "tactic:tac2def_mut"
-let tac2def_run = Entry.create "tactic:tac2def_run"
-let tac2mode = Entry.create "vernac:ltac2_command"
-
-let ltac1_expr = Pltac.tactic_expr
-
-let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
-let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
-let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
-let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
-let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
-
-let pattern_of_qualid qid =
-  if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, [])
-  else
-    let open Libnames in
-    if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ CPatVar (Name (qualid_basename qid))
-    else
-      CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error")
-
-GEXTEND Gram
-  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
-          tac2def_mut tac2def_run;
-  tac2pat:
-    [ "1" LEFTA
-      [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
-        if Tac2env.is_constructor qid then
-          CAst.make ~loc:!@loc @@ CPatRef (RelId qid, pl)
-        else
-          CErrors.user_err ~loc:!@loc (Pp.str "Syntax error")
-      | qid = Prim.qualid -> pattern_of_qualid qid
-      | "["; "]" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), [])
-      | p1 = tac2pat; "::"; p2 = tac2pat ->
-        CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])
-      ]
-    | "0"
-      [ "_" -> CAst.make ~loc:!@loc @@ CPatVar Anonymous
-      | "()" -> CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
-      | qid = Prim.qualid -> pattern_of_qualid qid
-      | "("; p = atomic_tac2pat; ")" -> p
-    ] ]
-  ;
-  atomic_tac2pat:
-    [ [ ->
-        CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple 0), [])
-      | p = tac2pat; ":"; t = tac2type ->
-        CAst.make ~loc:!@loc @@ CPatCnv (p, t)
-      | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
-        let pl = p :: pl in
-        CAst.make ~loc:!@loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl)
-      | p = tac2pat -> p
-    ] ]
-  ;
-  tac2expr:
-    [ "6" RIGHTA
-        [ e1 = SELF; ";"; e2 = SELF -> CAst.make ~loc:!@loc @@ CTacSeq (e1, e2) ]
-    | "5"
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
-        CAst.make ~loc:!@loc @@ CTacFun (it, body)
-      | "let"; isrec = rec_flag;
-          lc = LIST1 let_clause SEP "with"; "in";
-          e = tac2expr LEVEL "6" ->
-        CAst.make ~loc:!@loc @@ CTacLet (isrec, lc, e)
-      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
-        CAst.make ~loc:!@loc @@ CTacCse (e, bl)
-      ]
-    | "4" LEFTA [ ]
-    | "::" RIGHTA
-      [ e1 = tac2expr; "::"; e2 = tac2expr ->
-        CAst.make ~loc:!@loc @@ CTacApp (CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2])
-      ]
-    | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
-        let el = e0 :: el in
-        CAst.make ~loc:!@loc @@ CTacApp (CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) ]
-    | "1" LEFTA
-      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
-        CAst.make ~loc:!@loc @@ CTacApp (e, el)
-      | e = SELF; ".("; qid = Prim.qualid; ")" ->
-        CAst.make ~loc:!@loc @@ CTacPrj (e, RelId qid)
-      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
-        CAst.make ~loc:!@loc @@ CTacSet (e, RelId qid, r) ]
-    | "0"
-      [ "("; a = SELF; ")" -> a
-      | "("; a = SELF; ":"; t = tac2type; ")" ->
-        CAst.make ~loc:!@loc @@ CTacCnv (a, t)
-      | "()" ->
-        CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
-      | "("; ")" ->
-        CAst.make ~loc:!@loc @@ CTacCst (AbsKn (Tuple 0))
-      | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
-        Tac2quote.of_list ~loc:!@loc (fun x -> x) a
-      | "{"; a = tac2rec_fieldexprs; "}" ->
-        CAst.make ~loc:!@loc @@ CTacRec a
-      | a = tactic_atom -> a ]
-    ]
-  ;
-  branches:
-  [ [ -> []
-    | "|"; bl = LIST1 branch SEP "|" -> bl
-    | bl = LIST1 branch SEP "|" -> bl ]
-  ]
-  ;
-  branch:
-  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> (pat, e) ] ]
-  ;
-  rec_flag:
-    [ [ IDENT "rec" -> true
-      | -> false ] ]
-  ;
-  mut_flag:
-    [ [ IDENT "mutable" -> true
-      | -> false ] ]
-  ;
-  typ_param:
-    [ [ "'"; id = Prim.ident -> id ] ]
-  ;
-  tactic_atom:
-    [ [ n = Prim.integer -> CAst.make ~loc:!@loc @@ CTacAtm (AtmInt n)
-      | s = Prim.string -> CAst.make ~loc:!@loc @@ CTacAtm (AtmStr s)
-      | qid = Prim.qualid ->
-        if Tac2env.is_constructor qid then
-          CAst.make ~loc:!@loc @@ CTacCst (RelId qid)
-        else
-          CAst.make ~loc:!@loc @@ CTacRef (RelId qid)
-      | "@"; id = Prim.ident -> Tac2quote.of_ident (CAst.make ~loc:!@loc id)
-      | "&"; id = lident -> Tac2quote.of_hyp ~loc:!@loc id
-      | "'"; c = Constr.constr -> inj_open_constr !@loc c
-      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_constr c
-      | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_open_constr c
-      | IDENT "ident"; ":"; "("; c = lident; ")" -> Tac2quote.of_ident c
-      | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
-      | IDENT "reference"; ":"; "("; c = globref; ")" -> inj_reference !@loc c
-      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> inj_ltac1 !@loc qid
-    ] ]
-  ;
-  let_clause:
-    [ [ binder = let_binder; ":="; te = tac2expr ->
-        let (pat, fn) = binder in
-        let te = match fn with
-        | None -> te
-        | Some args -> CAst.make ~loc:!@loc @@ CTacFun (args, te)
-        in
-        (pat, te)
-    ] ]
-  ;
-  let_binder:
-    [ [ pats = LIST1 input_fun ->
-        match pats with
-        | [{CAst.v=CPatVar _} as pat] -> (pat, None)
-        | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, Some args)
-        | [pat] -> (pat, None)
-        | _ -> CErrors.user_err ~loc:!@loc (str "Invalid pattern")
-    ] ]
-  ;
-  tac2type:
-    [ "5" RIGHTA
-      [ t1 = tac2type; "->"; t2 = tac2type -> CAst.make ~loc:!@loc @@ CTypArrow (t1, t2) ]
-    | "2"
-      [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
-        let tl = t :: tl in
-        CAst.make ~loc:!@loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) ]
-    | "1" LEFTA
-      [ t = SELF; qid = Prim.qualid -> CAst.make ~loc:!@loc @@ CTypRef (RelId qid, [t]) ]
-    | "0"
-      [ "("; t = tac2type LEVEL "5"; ")"  -> t
-      | id = typ_param -> CAst.make ~loc:!@loc @@ CTypVar (Name id)
-      | "_" -> CAst.make ~loc:!@loc @@ CTypVar Anonymous
-      | qid = Prim.qualid -> CAst.make ~loc:!@loc @@ CTypRef (RelId qid, [])
-      | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
-        CAst.make ~loc:!@loc @@ CTypRef (RelId qid, p) ]
-    ];
-  locident:
-    [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
-  ;
-  binder:
-    [ [ "_" -> CAst.make ~loc:!@loc Anonymous
-      | l = Prim.ident -> CAst.make ~loc:!@loc (Name l) ] ]
-  ;
-  input_fun:
-    [ [ b = tac2pat LEVEL "0" -> b ] ]
-  ;
-  tac2def_body:
-    [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
-        let e = if List.is_empty it then e else CAst.make ~loc:!@loc @@ CTacFun (it, e) in
-        (name, e)
-    ] ]
-  ;
-  tac2def_val:
-    [ [ mut = mut_flag; isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
-        StrVal (mut, isrec, l)
-    ] ]
-  ;
-  tac2def_mut:
-    [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> StrMut (qid, e) ] ]
-  ;
-  tac2def_run:
-    [ [ "Eval"; e = tac2expr -> StrRun e ] ]
-  ;
-  tac2typ_knd:
-    [ [ t = tac2type -> CTydDef (Some t)
-      | "["; ".."; "]" -> CTydOpn
-      | "["; t = tac2alg_constructors; "]" -> CTydAlg t
-      | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ]
-  ;
-  tac2alg_constructors:
-    [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> cs
-      | cs = LIST0 tac2alg_constructor SEP "|" -> cs ] ]
-  ;
-  tac2alg_constructor:
-    [ [ c = Prim.ident -> (c, [])
-      | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ]
-  ;
-  tac2rec_fields:
-    [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> f :: l
-      | f = tac2rec_field; ";" -> [f]
-      | f = tac2rec_field -> [f]
-      | -> [] ] ]
-  ;
-  tac2rec_field:
-    [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
-  ;
-  tac2rec_fieldexprs:
-    [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l
-      | f = tac2rec_fieldexpr; ";" -> [f]
-      | f = tac2rec_fieldexpr-> [f]
-      | -> [] ] ]
-  ;
-  tac2rec_fieldexpr:
-    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> RelId qid, e ] ]
-  ;
-  tac2typ_prm:
-    [ [ -> []
-      | id = typ_param -> [CAst.make ~loc:!@loc id]
-      | "("; ids = LIST1 [ id = typ_param -> CAst.make ~loc:!@loc id ] SEP "," ;")" -> ids
-    ] ]
-  ;
-  tac2typ_def:
-    [ [ prm = tac2typ_prm; id = Prim.qualid; (r, e) = tac2type_body -> (id, r, (prm, e)) ] ]
-  ;
-  tac2type_body:
-    [ [ -> false, CTydDef None
-      | ":="; e = tac2typ_knd -> false, e
-      | "::="; e = tac2typ_knd -> true, e
-    ] ]
-  ;
-  tac2def_typ:
-    [ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" ->
-        StrTyp (isrec, l)
-    ] ]
-  ;
-  tac2def_ext:
-    [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
-        plugin = Prim.string; name = Prim.string ->
-        let ml = { mltac_plugin = plugin; mltac_tactic = name } in
-        StrPrm (id, t, ml)
-    ] ]
-  ;
-  syn_node:
-    [ [ "_" -> CAst.make ~loc:!@loc None
-      | id = Prim.ident -> CAst.make ~loc:!@loc (Some id)
-    ] ]
-  ;
-  sexpr:
-    [ [ s = Prim.string -> SexprStr (CAst.make ~loc:!@loc s)
-      | n = Prim.integer -> SexprInt (CAst.make ~loc:!@loc n)
-      | id = syn_node -> SexprRec (!@loc, id, [])
-      | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
-        SexprRec (!@loc, id, tok)
-    ] ]
-  ;
-  syn_level:
-    [ [ -> None
-      | ":"; n = Prim.integer -> Some n
-    ] ]
-  ;
-  tac2def_syn:
-    [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
-        e = tac2expr ->
-        StrSyn (toks, n, e)
-    ] ]
-  ;
-  lident:
-    [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
-  ;
-  globref:
-    [ [ "&"; id = Prim.ident -> CAst.make ~loc:!@loc (QHypothesis id)
-      | qid = Prim.qualid -> CAst.make ~loc:!@loc @@ QReference qid
-    ] ]
-  ;
-END
-
-(** Quotation scopes used by notations *)
-
-open Tac2entries.Pltac
-
-let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
-
-GEXTEND Gram
-  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
-          q_conversion q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
-          q_destruction_arg q_reference q_with_bindings q_constr_matching
-          q_goal_matching q_hintdb q_move_location q_pose q_assert;
-  anti:
-    [ [ "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id) ] ]
-  ;
-  ident_or_anti:
-    [ [ id = lident -> QExpr id
-      | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
-    ] ]
-  ;
-  lident:
-    [ [ id = Prim.ident -> CAst.make ~loc:!@loc id ] ]
-  ;
-  lnatural:
-    [ [ n = Prim.natural -> CAst.make ~loc:!@loc n ] ]
-  ;
-  q_ident:
-    [ [ id = ident_or_anti -> id ] ]
-  ;
-  qhyp:
-    [ [ x = anti -> x
-      | n = lnatural -> QExpr (CAst.make ~loc:!@loc @@ QAnonHyp n)
-      | id = lident -> QExpr (CAst.make ~loc:!@loc @@ QNamedHyp id)
-    ] ]
-  ;
-  simple_binding:
-    [ [ "("; h = qhyp; ":="; c = Constr.lconstr; ")" ->
-        CAst.make ~loc:!@loc (h, c)
-    ] ]
-  ;
-  bindings:
-    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
-        CAst.make ~loc:!@loc @@ QExplicitBindings bl
-      | bl = LIST1 Constr.constr ->
-        CAst.make ~loc:!@loc @@ QImplicitBindings bl
-    ] ]
-  ;
-  q_bindings:
-    [ [ bl = bindings -> bl ] ]
-  ;
-  q_with_bindings:
-    [ [ bl = with_bindings -> bl ] ]
-  ;
-  intropatterns:
-    [ [ l = LIST0 nonsimple_intropattern -> CAst.make ~loc:!@loc l ]]
-  ;
-(*   ne_intropatterns: *)
-(*     [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
-(*   ; *)
-  or_and_intropattern:
-    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> CAst.make ~loc:!@loc @@ QIntroOrPattern tc
-      | "()" -> CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc [])
-      | "("; si = simple_intropattern; ")" -> CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc [si])
-      | "("; si = simple_intropattern; ",";
-             tc = LIST1 simple_intropattern SEP "," ; ")" ->
-             CAst.make ~loc:!@loc @@ QIntroAndPattern (CAst.make ~loc:!@loc (si::tc))
-      | "("; si = simple_intropattern; "&";
-	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
-	  (* (A & B & C) is translated into (A,(B,C)) *)
-	  let rec pairify = function
-	    | ([]|[_]|[_;_]) as l -> CAst.make ~loc:!@loc l
-	    | t::q ->
-              let q =
-                CAst.make ~loc:!@loc @@
-                  QIntroAction (CAst.make ~loc:!@loc @@
-                    QIntroOrAndPattern (CAst.make ~loc:!@loc @@
-                      QIntroAndPattern (pairify q)))
-              in
-              CAst.make ~loc:!@loc [t; q]
-	  in CAst.make ~loc:!@loc @@ QIntroAndPattern (pairify (si::tc)) ] ]
-  ;
-  equality_intropattern:
-    [ [ "->" -> CAst.make ~loc:!@loc @@ QIntroRewrite true
-      | "<-" -> CAst.make ~loc:!@loc @@ QIntroRewrite false
-      | "[="; tc = intropatterns; "]" -> CAst.make ~loc:!@loc @@ QIntroInjection tc ] ]
-  ;
-  naming_intropattern:
-    [ [ LEFTQMARK; id = lident ->
-        CAst.make ~loc:!@loc @@ QIntroFresh (QExpr id)
-      | "?$"; id = lident ->
-        CAst.make ~loc:!@loc @@ QIntroFresh (QAnti id)
-      | "?" ->
-        CAst.make ~loc:!@loc @@ QIntroAnonymous
-      | id = ident_or_anti ->
-        CAst.make ~loc:!@loc @@ QIntroIdentifier id
-    ] ]
-  ;
-  nonsimple_intropattern:
-    [ [ l = simple_intropattern -> l
-      | "*"  -> CAst.make ~loc:!@loc @@ QIntroForthcoming true
-      | "**" -> CAst.make ~loc:!@loc @@ QIntroForthcoming false ]]
-  ;
-  simple_intropattern:
-    [ [ pat = simple_intropattern_closed ->
-(*         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *)
-        (** TODO: handle %pat *)
-        pat
-    ] ]
-  ;
-  simple_intropattern_closed:
-    [ [ pat = or_and_intropattern ->
-        CAst.make ~loc:!@loc @@ QIntroAction (CAst.make ~loc:!@loc @@ QIntroOrAndPattern pat)
-      | pat = equality_intropattern ->
-        CAst.make ~loc:!@loc @@ QIntroAction pat
-      | "_" ->
-        CAst.make ~loc:!@loc @@ QIntroAction (CAst.make ~loc:!@loc @@ QIntroWildcard)
-      | pat = naming_intropattern ->
-        CAst.make ~loc:!@loc @@ QIntroNaming pat
-    ] ]
-  ;
-  q_intropatterns:
-    [ [ ipat = intropatterns -> ipat ] ]
-  ;
-  q_intropattern:
-    [ [ ipat = simple_intropattern -> ipat ] ]
-  ;
-  nat_or_anti:
-    [ [ n = lnatural -> QExpr n
-      | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
-    ] ]
-  ;
-  eqn_ipat:
-    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some pat
-      | -> None
-    ] ]
-  ;
-  with_bindings:
-    [ [ "with"; bl = bindings -> bl | -> CAst.make ~loc:!@loc @@ QNoBindings ] ]
-  ;
-  constr_with_bindings:
-    [ [ c = Constr.constr; l = with_bindings -> CAst.make ~loc:!@loc @@ (c, l) ] ]
-  ;
-  destruction_arg:
-    [ [ n = lnatural -> CAst.make ~loc:!@loc @@ QElimOnAnonHyp n
-      | id = lident -> CAst.make ~loc:!@loc @@ QElimOnIdent id
-      | c = constr_with_bindings -> CAst.make ~loc:!@loc @@ QElimOnConstr c
-    ] ]
-  ;
-  q_destruction_arg:
-    [ [ arg = destruction_arg -> arg ] ]
-  ;
-  as_or_and_ipat:
-    [ [ "as"; ipat = or_and_intropattern -> Some ipat
-      | -> None
-    ] ]
-  ;
-  occs_nums:
-    [ [ nl = LIST1 nat_or_anti -> CAst.make ~loc:!@loc @@ QOnlyOccurrences nl
-      | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
-        CAst.make ~loc:!@loc @@ QAllOccurrencesBut (n::nl)
-    ] ]
-  ;
-  occs:
-    [ [ "at"; occs = occs_nums -> occs | -> CAst.make ~loc:!@loc QAllOccurrences ] ]
-  ;
-  hypident:
-    [ [ id = ident_or_anti ->
-          id,Locus.InHyp
-      | "("; IDENT "type"; IDENT "of"; id = ident_or_anti; ")" ->
-	  id,Locus.InHypTypeOnly
-      | "("; IDENT "value"; IDENT "of"; id = ident_or_anti; ")" ->
-	  id,Locus.InHypValueOnly
-    ] ]
-  ;
-  hypident_occ:
-    [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
-  ;
-  in_clause:
-    [ [ "*"; occs=occs ->
-        { q_onhyps = None; q_concl_occs = occs }
-      | "*"; "|-"; occs = concl_occ ->
-        { q_onhyps = None; q_concl_occs = occs }
-      | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
-        { q_onhyps = Some hl; q_concl_occs = occs }
-      | hl = LIST0 hypident_occ SEP "," ->
-        { q_onhyps = Some hl; q_concl_occs = CAst.make ~loc:!@loc QNoOccurrences }
-    ] ]
-  ;
-  clause:
-    [ [ "in"; cl = in_clause -> CAst.make ~loc:!@loc @@ cl
-      | "at"; occs = occs_nums ->
-        CAst.make ~loc:!@loc @@ { q_onhyps = Some []; q_concl_occs = occs }
-    ] ]
-  ;
-  q_clause:
-    [ [ cl = clause -> cl ] ]
-  ;
-  concl_occ:
-    [ [ "*"; occs = occs -> occs
-      | -> CAst.make ~loc:!@loc QNoOccurrences
-    ] ]
-  ;
-  induction_clause:
-    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
-        cl = OPT clause ->
-        CAst.make ~loc:!@loc @@ {
-          indcl_arg = c;
-          indcl_eqn = eq;
-          indcl_as = pat;
-          indcl_in = cl;
-        }
-    ] ]
-  ;
-  q_induction_clause:
-    [ [ cl = induction_clause -> cl ] ]
-  ;
-  conversion:
-    [ [ c = Constr.constr ->
-        CAst.make ~loc:!@loc @@ QConvert c
-      | c1 = Constr.constr; "with"; c2 = Constr.constr ->
-        CAst.make ~loc:!@loc @@ QConvertWith (c1, c2)
-    ] ]
-  ;
-  q_conversion:
-    [ [ c = conversion -> c ] ]
-  ;
-  orient:
-    [ [ "->" -> CAst.make ~loc:!@loc (Some true)
-      | "<-" -> CAst.make ~loc:!@loc (Some false)
-      | -> CAst.make ~loc:!@loc None
-    ]]
-  ;
-  rewriter:
-    [ [ "!"; c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QRepeatPlus,c)
-      | ["?"| LEFTQMARK]; c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QRepeatStar,c)
-      | n = lnatural; "!"; c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QPrecisely n,c)
-      |	n = lnatural; ["?" | LEFTQMARK]; c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QUpTo n,c)
-      | n = lnatural; c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QPrecisely n,c)
-      | c = constr_with_bindings ->
-        (CAst.make ~loc:!@loc @@ QPrecisely (CAst.make 1), c)
-      ] ]
-  ;
-  oriented_rewriter:
-    [ [ b = orient; (m, c) = rewriter ->
-      CAst.make ~loc:!@loc @@ {
-        rew_orient = b;
-        rew_repeat = m;
-        rew_equatn = c;
-      }
-    ] ]
-  ;
-  q_rewriting:
-    [ [ r = oriented_rewriter -> r ] ]
-  ;
-  tactic_then_last:
-    [ [ "|"; lta = LIST0 OPT tac2expr LEVEL "6" SEP "|" -> lta
-      | -> []
-    ] ]
-  ;
-  tactic_then_gen:
-    [ [ ta = tac2expr; "|"; (first,last) = tactic_then_gen -> (Some ta :: first, last)
-      | ta = tac2expr; ".."; l = tactic_then_last -> ([], Some (Some ta, l))
-      | ".."; l = tactic_then_last -> ([], Some (None, l))
-      | ta = tac2expr -> ([Some ta], None)
-      | "|"; (first,last) = tactic_then_gen -> (None :: first, last)
-      | -> ([None], None)
-    ] ]
-  ;
-  q_dispatch:
-    [ [ d = tactic_then_gen -> CAst.make ~loc:!@loc d ] ]
-  ;
-  q_occurrences:
-    [ [ occs = occs -> occs ] ]
-  ;
-  red_flag:
-    [ [ IDENT "beta" -> CAst.make ~loc:!@loc @@ QBeta
-      | IDENT "iota" -> CAst.make ~loc:!@loc @@ QIota
-      | IDENT "match" -> CAst.make ~loc:!@loc @@ QMatch
-      | IDENT "fix" -> CAst.make ~loc:!@loc @@ QFix
-      | IDENT "cofix" -> CAst.make ~loc:!@loc @@ QCofix
-      | IDENT "zeta" -> CAst.make ~loc:!@loc @@ QZeta
-      | IDENT "delta"; d = delta_flag -> d
-    ] ]
-  ;
-  refglobal:
-    [ [ "&"; id = Prim.ident -> QExpr (CAst.make ~loc:!@loc @@ QHypothesis id)
-      | qid = Prim.qualid -> QExpr (CAst.make ~loc:!@loc @@ QReference qid)
-      | "$"; id = Prim.ident -> QAnti (CAst.make ~loc:!@loc id)
-    ] ]
-  ;
-  q_reference:
-    [ [ r = refglobal -> r ] ]
-  ;
-  refglobals:
-    [ [ gl = LIST1 refglobal -> CAst.make ~loc:!@loc gl ] ]
-  ;
-  delta_flag:
-    [ [ "-"; "["; idl = refglobals; "]" -> CAst.make ~loc:!@loc @@ QDeltaBut idl
-      | "["; idl = refglobals; "]" -> CAst.make ~loc:!@loc @@ QConst idl
-      | -> CAst.make ~loc:!@loc @@ QDeltaBut (CAst.make ~loc:!@loc [])
-    ] ]
-  ;
-  strategy_flag:
-    [ [ s = LIST1 red_flag -> CAst.make ~loc:!@loc s
-      | d = delta_flag ->
-        CAst.make ~loc:!@loc
-          [CAst.make ~loc:!@loc QBeta; CAst.make ~loc:!@loc QIota; CAst.make ~loc:!@loc QZeta; d]
-    ] ]
-  ;
-  q_strategy_flag:
-    [ [ flag = strategy_flag -> flag ] ]
-  ;
-  hintdb:
-    [ [ "*" -> CAst.make ~loc:!@loc @@ QHintAll
-      | l = LIST1 ident_or_anti -> CAst.make ~loc:!@loc @@ QHintDbs l
-    ] ]
-  ;
-  q_hintdb:
-    [ [ db = hintdb -> db ] ]
-  ;
-  match_pattern:
-    [ [ IDENT "context";  id = OPT Prim.ident;
-          "["; pat = Constr.lconstr_pattern; "]" -> CAst.make ~loc:!@loc @@ QConstrMatchContext (id, pat)
-      | pat = Constr.lconstr_pattern -> CAst.make ~loc:!@loc @@ QConstrMatchPattern pat ] ]
-  ;
-  match_rule:
-    [ [ mp = match_pattern; "=>"; tac = tac2expr ->
-        CAst.make ~loc:!@loc @@ (mp, tac)
-    ] ]
-  ;
-  match_list:
-    [ [ mrl = LIST1 match_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl
-      | "|"; mrl = LIST1 match_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl ] ]
-  ;
-  q_constr_matching:
-    [ [ m = match_list -> m ] ]
-  ;
-  gmatch_hyp_pattern:
-    [ [ na = Prim.name; ":"; pat = match_pattern -> (na, pat) ] ]
-  ;
-  gmatch_pattern:
-    [ [ "["; hl = LIST0 gmatch_hyp_pattern SEP ","; "|-"; p = match_pattern; "]" ->
-        CAst.make ~loc:!@loc @@ {
-          q_goal_match_concl = p;
-          q_goal_match_hyps = hl;
-        }
-    ] ]
-  ;
-  gmatch_rule:
-    [ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
-        CAst.make ~loc:!@loc @@ (mp, tac)
-    ] ]
-  ;
-  gmatch_list:
-    [ [ mrl = LIST1 gmatch_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl
-      | "|"; mrl = LIST1 gmatch_rule SEP "|" -> CAst.make ~loc:!@loc @@ mrl ] ]
-  ;
-  q_goal_matching:
-    [ [ m = gmatch_list -> m ] ]
-  ;
-  move_location:
-    [ [ "at"; IDENT "top" -> CAst.make ~loc:!@loc @@ QMoveFirst
-      | "at"; IDENT "bottom" -> CAst.make ~loc:!@loc @@ QMoveLast
-      | IDENT "after"; id = ident_or_anti -> CAst.make ~loc:!@loc @@ QMoveAfter id
-      | IDENT "before"; id = ident_or_anti -> CAst.make ~loc:!@loc @@ QMoveBefore id
-    ] ]
-  ;
-  q_move_location:
-    [ [ mv = move_location -> mv ] ]
-  ;
-  as_name:
-    [ [ -> None
-      | "as"; id = ident_or_anti -> Some id
-    ] ]
-  ;
-  pose:
-    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
-        CAst.make ~loc:!@loc (Some id, c)
-      | c = Constr.constr; na = as_name -> CAst.make ~loc:!@loc (na, c)
-    ] ]
-  ;
-  q_pose:
-    [ [ p = pose -> p ] ]
-  ;
-  as_ipat:
-    [ [ "as"; ipat = simple_intropattern -> Some ipat
-      | -> None
-    ] ]
-  ;
-  by_tactic:
-    [ [ "by"; tac = tac2expr -> Some tac
-      | -> None
-    ] ]
-  ;
-  assertion:
-    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
-        CAst.make ~loc:!@loc (QAssertValue (id, c))
-      | test_lpar_id_colon; "("; id = ident_or_anti; ":"; c = Constr.lconstr; ")"; tac = by_tactic ->
-        let loc = !@loc in
-        let ipat = CAst.make ~loc @@ QIntroNaming (CAst.make ~loc @@ QIntroIdentifier id) in
-        CAst.make ~loc (QAssertType (Some ipat, c, tac))
-      | c = Constr.constr; ipat = as_ipat; tac = by_tactic ->
-        CAst.make ~loc:!@loc (QAssertType (ipat, c, tac))
-    ] ]
-  ;
-  q_assert:
-    [ [ a = assertion -> a ] ]
-  ;
-END
-
-(** Extension of constr syntax *)
-
-let () = Hook.set Tac2entries.register_constr_quotations begin fun () ->
-GEXTEND Gram
-  Pcoq.Constr.operconstr: LEVEL "0"
-    [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
-        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
-      | test_ampersand_ident; "&"; id = Prim.ident ->
-        let tac = Tac2quote.of_exact_hyp ~loc:!@loc (CAst.make ~loc:!@loc id) in
-        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
-      | test_dollar_ident; "$"; id = Prim.ident ->
-        let id = Loc.tag ~loc:!@loc id in
-        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
-        CAst.make ~loc:!@loc (CHole (None, Namegen.IntroAnonymous, Some arg))
-    ] ]
-  ;
-END
-end
-
-let pr_ltac2entry _ = mt () (** FIXME *)
-let pr_ltac2expr _ = mt () (** FIXME *)
-
-VERNAC ARGUMENT EXTEND ltac2_entry
-PRINTED BY pr_ltac2entry
-| [ tac2def_val(v) ] -> [ v ]
-| [ tac2def_typ(t) ] -> [ t ]
-| [ tac2def_ext(e) ] -> [ e ]
-| [ tac2def_syn(e) ] -> [ e ]
-| [ tac2def_mut(e) ] -> [ e ]
-| [ tac2def_run(e) ] -> [ e ]
-END
-
-let classify_ltac2 = function
-| StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
-| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff
-
-VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTactic2Definition
-| [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
-    fun ~atts ~st ->
-    Tac2entries.register_struct ?local:(Attributes.only_locality atts) e;
-    st
-  ]
-END
-
-let _ =
-  let mode = {
-    Proof_global.name = "Ltac2";
-    set = (fun () -> Pvernac.set_command_entry tac2mode);
-    reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode));
-  } in
-  Proof_global.register_proof_mode mode
-
-VERNAC ARGUMENT EXTEND ltac2_expr
-PRINTED BY pr_ltac2expr
-| [ tac2expr(e) ] -> [ e ]
-END
-
-open G_ltac
-open Vernac_classifier
-
-VERNAC tac2mode EXTEND VernacLtac2
-| [ - ltac2_expr(t) ltac_use_default(default) ] =>
-    [ classify_as_proofstep ] -> [
-(*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
-    Tac2entries.call ~default t
-  ]
-END
-
-open Stdarg
-
-VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
-| [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ]
-END
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
new file mode 100644
index 0000000000..5aad77596d
--- /dev/null
+++ b/src/g_ltac2.mlg
@@ -0,0 +1,936 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+{
+
+open Pp
+open Util
+open Names
+open Tok
+open Pcoq
+open Attributes
+open Constrexpr
+open Tac2expr
+open Tac2qexpr
+open Ltac_plugin
+
+let err () = raise Stream.Failure
+
+type lookahead = int -> Tok.t Stream.t -> int option
+
+let entry_of_lookahead s (lk : lookahead) =
+  let run strm = match lk 0 strm with None -> err () | Some _ -> () in
+  Gram.Entry.of_parser s run
+
+let (>>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
+| None -> None
+| Some n -> lk2 n strm
+
+let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
+| None -> lk2 n strm
+| Some n -> Some n
+
+let lk_kw kw n strm = match stream_nth n strm with
+| KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
+| _ -> None
+
+let lk_ident n strm = match stream_nth n strm with
+| IDENT _ -> Some (n + 1)
+| _ -> None
+
+let lk_int n strm = match stream_nth n strm with
+| INT _ -> Some (n + 1)
+| _ -> None
+
+let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident)
+
+(* lookahead for (x:=t), (?x:=t) and (1:=t) *)
+let test_lpar_idnum_coloneq =
+  entry_of_lookahead "test_lpar_idnum_coloneq" begin
+    lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":="
+  end
+
+(* lookahead for (x:t), (?x:t) *)
+let test_lpar_id_colon =
+  entry_of_lookahead "test_lpar_id_colon" begin
+    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
+  end
+
+(* Hack to recognize "(x := t)" and "($x := t)" *)
+let test_lpar_id_coloneq =
+  entry_of_lookahead "test_lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
+  end
+
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+  entry_of_lookahead "test_lpar_id_rpar" begin
+    lk_kw "(" >> lk_ident >> lk_kw ")"
+  end
+
+let test_ampersand_ident =
+  entry_of_lookahead "test_ampersand_ident" begin
+    lk_kw "&" >> lk_ident
+  end
+
+let test_dollar_ident =
+  entry_of_lookahead "test_dollar_ident" begin
+    lk_kw "$" >> lk_ident
+  end
+
+let tac2expr = Tac2entries.Pltac.tac2expr
+let tac2type = Entry.create "tactic:tac2type"
+let tac2def_val = Entry.create "tactic:tac2def_val"
+let tac2def_typ = Entry.create "tactic:tac2def_typ"
+let tac2def_ext = Entry.create "tactic:tac2def_ext"
+let tac2def_syn = Entry.create "tactic:tac2def_syn"
+let tac2def_mut = Entry.create "tactic:tac2def_mut"
+let tac2def_run = Entry.create "tactic:tac2def_run"
+let tac2mode = Entry.create "vernac:ltac2_command"
+
+let ltac1_expr = Pltac.tactic_expr
+
+let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
+let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
+let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
+let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
+let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
+
+let pattern_of_qualid qid =
+  if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, [])
+  else
+    let open Libnames in
+    if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ CPatVar (Name (qualid_basename qid))
+    else
+      CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error")
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
+          tac2def_mut tac2def_run;
+  tac2pat:
+    [ "1" LEFTA
+      [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
+        if Tac2env.is_constructor qid then
+          CAst.make ~loc @@ CPatRef (RelId qid, pl)
+        else
+          CErrors.user_err ~loc (Pp.str "Syntax error") }
+      | qid = Prim.qualid -> { pattern_of_qualid qid }
+      | "["; "]" -> { CAst.make ~loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), []) }
+      | p1 = tac2pat; "::"; p2 = tac2pat ->
+        { CAst.make ~loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])}
+      ]
+    | "0"
+      [ "_" -> { CAst.make ~loc @@ CPatVar Anonymous }
+      | "()" -> { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
+      | qid = Prim.qualid -> { pattern_of_qualid qid }
+      | "("; p = atomic_tac2pat; ")" -> { p }
+    ] ]
+  ;
+  atomic_tac2pat:
+    [ [ ->
+        { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
+      | p = tac2pat; ":"; t = tac2type ->
+        { CAst.make ~loc @@ CPatCnv (p, t) }
+      | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
+        { let pl = p :: pl in
+          CAst.make ~loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl) }
+      | p = tac2pat -> { p }
+    ] ]
+  ;
+  tac2expr:
+    [ "6" RIGHTA
+        [ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ]
+    | "5"
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
+        { CAst.make ~loc @@ CTacFun (it, body) }
+      | "let"; isrec = rec_flag;
+          lc = LIST1 let_clause SEP "with"; "in";
+          e = tac2expr LEVEL "6" ->
+        { CAst.make ~loc @@ CTacLet (isrec, lc, e) }
+      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
+        { CAst.make ~loc @@ CTacCse (e, bl) }
+      ]
+    | "4" LEFTA [ ]
+    | "::" RIGHTA
+      [ e1 = tac2expr; "::"; e2 = tac2expr ->
+        { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
+      ]
+    | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
+        { let el = e0 :: el in
+          CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ]
+    | "1" LEFTA
+      [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
+        { CAst.make ~loc @@ CTacApp (e, el) }
+      | e = SELF; ".("; qid = Prim.qualid; ")" ->
+        { CAst.make ~loc @@ CTacPrj (e, RelId qid) }
+      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
+        { CAst.make ~loc @@ CTacSet (e, RelId qid, r) } ]
+    | "0"
+      [ "("; a = SELF; ")" -> { a }
+      | "("; a = SELF; ":"; t = tac2type; ")" ->
+        { CAst.make ~loc @@ CTacCnv (a, t) }
+      | "()" ->
+        { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
+      | "("; ")" ->
+        { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
+      | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
+        { Tac2quote.of_list ~loc (fun x -> x) a }
+      | "{"; a = tac2rec_fieldexprs; "}" ->
+        { CAst.make ~loc @@ CTacRec a }
+      | a = tactic_atom -> { a } ]
+    ]
+  ;
+  branches:
+  [ [ -> { [] }
+    | "|"; bl = LIST1 branch SEP "|" -> { bl }
+    | bl = LIST1 branch SEP "|" -> { bl } ]
+  ]
+  ;
+  branch:
+  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> { (pat, e) } ] ]
+  ;
+  rec_flag:
+    [ [ IDENT "rec" -> { true }
+      | -> { false } ] ]
+  ;
+  mut_flag:
+    [ [ IDENT "mutable" -> { true }
+      | -> { false } ] ]
+  ;
+  typ_param:
+    [ [ "'"; id = Prim.ident -> { id } ] ]
+  ;
+  tactic_atom:
+    [ [ n = Prim.integer -> { CAst.make ~loc @@ CTacAtm (AtmInt n) }
+      | s = Prim.string -> { CAst.make ~loc @@ CTacAtm (AtmStr s) }
+      | qid = Prim.qualid ->
+      { if Tac2env.is_constructor qid then
+          CAst.make ~loc @@ CTacCst (RelId qid)
+        else
+          CAst.make ~loc @@ CTacRef (RelId qid) }
+      | "@"; id = Prim.ident -> { Tac2quote.of_ident (CAst.make ~loc id) }
+      | "&"; id = lident -> { Tac2quote.of_hyp ~loc id }
+      | "'"; c = Constr.constr -> { inj_open_constr loc c }
+      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c }
+      | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c }
+      | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
+      | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
+      | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
+      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1 loc qid }
+    ] ]
+  ;
+  let_clause:
+    [ [ binder = let_binder; ":="; te = tac2expr ->
+      { let (pat, fn) = binder in
+        let te = match fn with
+        | None -> te
+        | Some args -> CAst.make ~loc @@ CTacFun (args, te)
+        in
+        (pat, te) }
+    ] ]
+  ;
+  let_binder:
+    [ [ pats = LIST1 input_fun ->
+      { match pats with
+        | [{CAst.v=CPatVar _} as pat] -> (pat, None)
+        | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, Some args)
+        | [pat] -> (pat, None)
+        | _ -> CErrors.user_err ~loc (str "Invalid pattern") }
+    ] ]
+  ;
+  tac2type:
+    [ "5" RIGHTA
+      [ t1 = tac2type; "->"; t2 = tac2type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
+    | "2"
+      [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
+      { let tl = t :: tl in
+        CAst.make ~loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) } ]
+    | "1" LEFTA
+      [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
+    | "0"
+      [ "("; t = tac2type LEVEL "5"; ")"  -> { t }
+      | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) }
+      | "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
+      | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
+      | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
+        { CAst.make ~loc @@ CTypRef (RelId qid, p) } ]
+    ];
+  locident:
+    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
+  ;
+  binder:
+    [ [ "_" -> { CAst.make ~loc Anonymous }
+      | l = Prim.ident -> { CAst.make ~loc (Name l) } ] ]
+  ;
+  input_fun:
+    [ [ b = tac2pat LEVEL "0" -> { b } ] ]
+  ;
+  tac2def_body:
+    [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
+      { let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in
+        (name, e) }
+    ] ]
+  ;
+  tac2def_val:
+    [ [ mut = mut_flag; isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
+        { StrVal (mut, isrec, l) }
+    ] ]
+  ;
+  tac2def_mut:
+    [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ]
+  ;
+  tac2def_run:
+    [ [ "Eval"; e = tac2expr -> { StrRun e } ] ]
+  ;
+  tac2typ_knd:
+    [ [ t = tac2type -> { CTydDef (Some t) }
+      | "["; ".."; "]" -> { CTydOpn }
+      | "["; t = tac2alg_constructors; "]" -> { CTydAlg t }
+      | "{"; t = tac2rec_fields; "}"-> { CTydRec t } ] ]
+  ;
+  tac2alg_constructors:
+    [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> { cs }
+      | cs = LIST0 tac2alg_constructor SEP "|" -> { cs } ] ]
+  ;
+  tac2alg_constructor:
+    [ [ c = Prim.ident -> { (c, []) }
+      | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> { (c, args) } ] ]
+  ;
+  tac2rec_fields:
+    [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> { f :: l }
+      | f = tac2rec_field; ";" -> { [f] }
+      | f = tac2rec_field -> { [f] }
+      | -> { [] } ] ]
+  ;
+  tac2rec_field:
+    [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> { (id, mut, t) } ] ]
+  ;
+  tac2rec_fieldexprs:
+    [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> { f :: l }
+      | f = tac2rec_fieldexpr; ";" -> { [f] }
+      | f = tac2rec_fieldexpr-> { [f] }
+      | -> { [] } ] ]
+  ;
+  tac2rec_fieldexpr:
+    [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> { RelId qid, e } ] ]
+  ;
+  tac2typ_prm:
+    [ [ -> { [] }
+      | id = typ_param -> { [CAst.make ~loc id] }
+      | "("; ids = LIST1 [ id = typ_param -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
+    ] ]
+  ;
+  tac2typ_def:
+    [ [ prm = tac2typ_prm; id = Prim.qualid; b = tac2type_body -> { let (r, e) = b in (id, r, (prm, e)) } ] ]
+  ;
+  tac2type_body:
+    [ [ -> { false, CTydDef None }
+      | ":="; e = tac2typ_knd -> { false, e }
+      | "::="; e = tac2typ_knd -> { true, e }
+    ] ]
+  ;
+  tac2def_typ:
+    [ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" ->
+        { StrTyp (isrec, l) }
+    ] ]
+  ;
+  tac2def_ext:
+    [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
+        plugin = Prim.string; name = Prim.string ->
+      { let ml = { mltac_plugin = plugin; mltac_tactic = name } in
+        StrPrm (id, t, ml) }
+    ] ]
+  ;
+  syn_node:
+    [ [ "_" -> { CAst.make ~loc None }
+      | id = Prim.ident -> { CAst.make ~loc (Some id) }
+    ] ]
+  ;
+  sexpr:
+    [ [ s = Prim.string -> { SexprStr (CAst.make ~loc s) }
+      | n = Prim.integer -> { SexprInt (CAst.make ~loc n) }
+      | id = syn_node -> { SexprRec (loc, id, []) }
+      | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
+        { SexprRec (loc, id, tok) }
+    ] ]
+  ;
+  syn_level:
+    [ [ -> { None }
+      | ":"; n = Prim.integer -> { Some n }
+    ] ]
+  ;
+  tac2def_syn:
+    [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
+        e = tac2expr ->
+        { StrSyn (toks, n, e) }
+    ] ]
+  ;
+  lident:
+    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
+  ;
+  globref:
+    [ [ "&"; id = Prim.ident -> { CAst.make ~loc (QHypothesis id) }
+      | qid = Prim.qualid -> { CAst.make ~loc @@ QReference qid }
+    ] ]
+  ;
+END
+
+(** Quotation scopes used by notations *)
+
+{
+
+open Tac2entries.Pltac
+
+let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
+          q_conversion q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
+          q_destruction_arg q_reference q_with_bindings q_constr_matching
+          q_goal_matching q_hintdb q_move_location q_pose q_assert;
+  anti:
+    [ [ "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) } ] ]
+  ;
+  ident_or_anti:
+    [ [ id = lident -> { QExpr id }
+      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
+    ] ]
+  ;
+  lident:
+    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
+  ;
+  lnatural:
+    [ [ n = Prim.natural -> { CAst.make ~loc n } ] ]
+  ;
+  q_ident:
+    [ [ id = ident_or_anti -> { id } ] ]
+  ;
+  qhyp:
+    [ [ x = anti -> { x }
+      | n = lnatural -> { QExpr (CAst.make ~loc @@ QAnonHyp n) }
+      | id = lident -> { QExpr (CAst.make ~loc @@ QNamedHyp id) }
+    ] ]
+  ;
+  simple_binding:
+    [ [ "("; h = qhyp; ":="; c = Constr.lconstr; ")" ->
+        { CAst.make ~loc (h, c) }
+    ] ]
+  ;
+  bindings:
+    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
+        { CAst.make ~loc @@ QExplicitBindings bl }
+      | bl = LIST1 Constr.constr ->
+        { CAst.make ~loc @@ QImplicitBindings bl }
+    ] ]
+  ;
+  q_bindings:
+    [ [ bl = bindings -> { bl } ] ]
+  ;
+  q_with_bindings:
+    [ [ bl = with_bindings -> { bl } ] ]
+  ;
+  intropatterns:
+    [ [ l = LIST0 nonsimple_intropattern -> { CAst.make ~loc l } ] ]
+  ;
+(*   ne_intropatterns: *)
+(*     [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
+(*   ; *)
+  or_and_intropattern:
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { CAst.make ~loc @@ QIntroOrPattern tc }
+      | "()" -> { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc []) }
+      | "("; si = simple_intropattern; ")" -> { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc [si]) }
+      | "("; si = simple_intropattern; ",";
+             tc = LIST1 simple_intropattern SEP "," ; ")" ->
+             { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc (si::tc)) }
+      | "("; si = simple_intropattern; "&";
+	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+	  (* (A & B & C) is translated into (A,(B,C)) *)
+	{ let rec pairify = function
+	    | ([]|[_]|[_;_]) as l -> CAst.make ~loc l
+	    | t::q ->
+              let q =
+                CAst.make ~loc @@
+                  QIntroAction (CAst.make ~loc @@
+                    QIntroOrAndPattern (CAst.make ~loc @@
+                      QIntroAndPattern (pairify q)))
+              in
+              CAst.make ~loc [t; q]
+	  in CAst.make ~loc @@ QIntroAndPattern (pairify (si::tc)) } ] ]
+  ;
+  equality_intropattern:
+    [ [ "->" -> { CAst.make ~loc @@ QIntroRewrite true }
+      | "<-" -> { CAst.make ~loc @@ QIntroRewrite false }
+      | "[="; tc = intropatterns; "]" -> { CAst.make ~loc @@ QIntroInjection tc } ] ]
+  ;
+  naming_intropattern:
+    [ [ LEFTQMARK; id = lident ->
+        { CAst.make ~loc @@ QIntroFresh (QExpr id) }
+      | "?$"; id = lident ->
+        { CAst.make ~loc @@ QIntroFresh (QAnti id) }
+      | "?" ->
+        { CAst.make ~loc @@ QIntroAnonymous }
+      | id = ident_or_anti ->
+        { CAst.make ~loc @@ QIntroIdentifier id }
+    ] ]
+  ;
+  nonsimple_intropattern:
+    [ [ l = simple_intropattern -> { l }
+      | "*"  -> { CAst.make ~loc @@ QIntroForthcoming true }
+      | "**" -> { CAst.make ~loc @@ QIntroForthcoming false } ] ]
+  ;
+  simple_intropattern:
+    [ [ pat = simple_intropattern_closed ->
+(*         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *)
+        (** TODO: handle %pat *)
+        { pat }
+    ] ]
+  ;
+  simple_intropattern_closed:
+    [ [ pat = or_and_intropattern ->
+        { CAst.make ~loc @@ QIntroAction (CAst.make ~loc @@ QIntroOrAndPattern pat) }
+      | pat = equality_intropattern ->
+        { CAst.make ~loc @@ QIntroAction pat }
+      | "_" ->
+        { CAst.make ~loc @@ QIntroAction (CAst.make ~loc @@ QIntroWildcard) }
+      | pat = naming_intropattern ->
+        { CAst.make ~loc @@ QIntroNaming pat }
+    ] ]
+  ;
+  q_intropatterns:
+    [ [ ipat = intropatterns -> { ipat } ] ]
+  ;
+  q_intropattern:
+    [ [ ipat = simple_intropattern -> { ipat } ] ]
+  ;
+  nat_or_anti:
+    [ [ n = lnatural -> { QExpr n }
+      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
+    ] ]
+  ;
+  eqn_ipat:
+    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some pat }
+      | -> { None }
+    ] ]
+  ;
+  with_bindings:
+    [ [ "with"; bl = bindings -> { bl } | -> { CAst.make ~loc @@ QNoBindings } ] ]
+  ;
+  constr_with_bindings:
+    [ [ c = Constr.constr; l = with_bindings -> { CAst.make ~loc @@ (c, l) } ] ]
+  ;
+  destruction_arg:
+    [ [ n = lnatural -> { CAst.make ~loc @@ QElimOnAnonHyp n }
+      | id = lident -> { CAst.make ~loc @@ QElimOnIdent id }
+      | c = constr_with_bindings -> { CAst.make ~loc @@ QElimOnConstr c }
+    ] ]
+  ;
+  q_destruction_arg:
+    [ [ arg = destruction_arg -> { arg } ] ]
+  ;
+  as_or_and_ipat:
+    [ [ "as"; ipat = or_and_intropattern -> { Some ipat }
+      | -> { None }
+    ] ]
+  ;
+  occs_nums:
+    [ [ nl = LIST1 nat_or_anti -> { CAst.make ~loc @@ QOnlyOccurrences nl }
+      | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
+        { CAst.make ~loc @@ QAllOccurrencesBut (n::nl) }
+    ] ]
+  ;
+  occs:
+    [ [ "at"; occs = occs_nums -> { occs } | -> { CAst.make ~loc QAllOccurrences } ] ]
+  ;
+  hypident:
+    [ [ id = ident_or_anti ->
+        { id,Locus.InHyp }
+      | "("; IDENT "type"; IDENT "of"; id = ident_or_anti; ")" ->
+        { id,Locus.InHypTypeOnly }
+      | "("; IDENT "value"; IDENT "of"; id = ident_or_anti; ")" ->
+        { id,Locus.InHypValueOnly }
+    ] ]
+  ;
+  hypident_occ:
+    [ [ h=hypident; occs=occs -> { let (id,l) = h in ((occs,id),l) } ] ]
+  ;
+  in_clause:
+    [ [ "*"; occs=occs ->
+        { { q_onhyps = None; q_concl_occs = occs } }
+      | "*"; "|-"; occs = concl_occ ->
+        { { q_onhyps = None; q_concl_occs = occs } }
+      | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
+        { { q_onhyps = Some hl; q_concl_occs = occs } }
+      | hl = LIST0 hypident_occ SEP "," ->
+        { { q_onhyps = Some hl; q_concl_occs = CAst.make ~loc QNoOccurrences } }
+    ] ]
+  ;
+  clause:
+    [ [ "in"; cl = in_clause -> { CAst.make ~loc @@ cl }
+      | "at"; occs = occs_nums ->
+        { CAst.make ~loc @@ { q_onhyps = Some []; q_concl_occs = occs } }
+    ] ]
+  ;
+  q_clause:
+    [ [ cl = clause -> { cl } ] ]
+  ;
+  concl_occ:
+    [ [ "*"; occs = occs -> { occs }
+      | -> { CAst.make ~loc QNoOccurrences }
+    ] ]
+  ;
+  induction_clause:
+    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+        cl = OPT clause ->
+      { CAst.make ~loc @@ {
+          indcl_arg = c;
+          indcl_eqn = eq;
+          indcl_as = pat;
+          indcl_in = cl;
+        } }
+    ] ]
+  ;
+  q_induction_clause:
+    [ [ cl = induction_clause -> { cl } ] ]
+  ;
+  conversion:
+    [ [ c = Constr.constr ->
+        { CAst.make ~loc @@ QConvert c }
+      | c1 = Constr.constr; "with"; c2 = Constr.constr ->
+        { CAst.make ~loc @@ QConvertWith (c1, c2) }
+    ] ]
+  ;
+  q_conversion:
+    [ [ c = conversion -> { c } ] ]
+  ;
+  orient:
+    [ [ "->" -> { CAst.make ~loc (Some true) }
+      | "<-" -> { CAst.make ~loc (Some false) }
+      | -> { CAst.make ~loc None }
+    ]]
+  ;
+  rewriter:
+    [ [ "!"; c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QRepeatPlus,c) }
+      | [ "?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QRepeatStar,c) }
+      | n = lnatural; "!"; c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QPrecisely n,c) }
+      |	n = lnatural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QUpTo n,c) }
+      | n = lnatural; c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QPrecisely n,c) }
+      | c = constr_with_bindings ->
+        { (CAst.make ~loc @@ QPrecisely (CAst.make 1), c) }
+      ] ]
+  ;
+  oriented_rewriter:
+    [ [ b = orient; r = rewriter ->
+      { let (m, c) = r in
+        CAst.make ~loc @@ {
+        rew_orient = b;
+        rew_repeat = m;
+        rew_equatn = c;
+      } }
+    ] ]
+  ;
+  q_rewriting:
+    [ [ r = oriented_rewriter -> { r } ] ]
+  ;
+  tactic_then_last:
+    [ [ "|"; lta = LIST0 (OPT tac2expr LEVEL "6") SEP "|" -> { lta }
+      | -> { [] }
+    ] ]
+  ;
+  tactic_then_gen:
+    [ [ ta = tac2expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (Some ta :: first, last) }
+      | ta = tac2expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
+      | ".."; l = tactic_then_last -> { ([], Some (None, l)) }
+      | ta = tac2expr -> { ([Some ta], None) }
+      | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (None :: first, last) }
+      | -> { ([None], None) }
+    ] ]
+  ;
+  q_dispatch:
+    [ [ d = tactic_then_gen -> { CAst.make ~loc d } ] ]
+  ;
+  q_occurrences:
+    [ [ occs = occs -> { occs } ] ]
+  ;
+  red_flag:
+    [ [ IDENT "beta" -> { CAst.make ~loc @@ QBeta }
+      | IDENT "iota" -> { CAst.make ~loc @@ QIota }
+      | IDENT "match" -> { CAst.make ~loc @@ QMatch }
+      | IDENT "fix" -> { CAst.make ~loc @@ QFix }
+      | IDENT "cofix" -> { CAst.make ~loc @@ QCofix }
+      | IDENT "zeta" -> { CAst.make ~loc @@ QZeta }
+      | IDENT "delta"; d = delta_flag -> { d }
+    ] ]
+  ;
+  refglobal:
+    [ [ "&"; id = Prim.ident -> { QExpr (CAst.make ~loc @@ QHypothesis id) }
+      | qid = Prim.qualid -> { QExpr (CAst.make ~loc @@ QReference qid) }
+      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
+    ] ]
+  ;
+  q_reference:
+    [ [ r = refglobal -> { r } ] ]
+  ;
+  refglobals:
+    [ [ gl = LIST1 refglobal -> { CAst.make ~loc gl } ] ]
+  ;
+  delta_flag:
+    [ [ "-"; "["; idl = refglobals; "]" -> { CAst.make ~loc @@ QDeltaBut idl }
+      | "["; idl = refglobals; "]" -> { CAst.make ~loc @@ QConst idl }
+      | -> { CAst.make ~loc @@ QDeltaBut (CAst.make ~loc []) }
+    ] ]
+  ;
+  strategy_flag:
+    [ [ s = LIST1 red_flag -> { CAst.make ~loc s }
+      | d = delta_flag ->
+      { CAst.make ~loc
+          [CAst.make ~loc QBeta; CAst.make ~loc QIota; CAst.make ~loc QZeta; d] }
+    ] ]
+  ;
+  q_strategy_flag:
+    [ [ flag = strategy_flag -> { flag } ] ]
+  ;
+  hintdb:
+    [ [ "*" -> { CAst.make ~loc @@ QHintAll }
+      | l = LIST1 ident_or_anti -> { CAst.make ~loc @@ QHintDbs l }
+    ] ]
+  ;
+  q_hintdb:
+    [ [ db = hintdb -> { db } ] ]
+  ;
+  match_pattern:
+    [ [ IDENT "context";  id = OPT Prim.ident;
+          "["; pat = Constr.lconstr_pattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
+      | pat = Constr.lconstr_pattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
+  ;
+  match_rule:
+    [ [ mp = match_pattern; "=>"; tac = tac2expr ->
+        { CAst.make ~loc @@ (mp, tac) }
+    ] ]
+  ;
+  match_list:
+    [ [ mrl = LIST1 match_rule SEP "|" -> { CAst.make ~loc @@ mrl }
+      | "|"; mrl = LIST1 match_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
+  ;
+  q_constr_matching:
+    [ [ m = match_list -> { m } ] ]
+  ;
+  gmatch_hyp_pattern:
+    [ [ na = Prim.name; ":"; pat = match_pattern -> { (na, pat) } ] ]
+  ;
+  gmatch_pattern:
+    [ [ "["; hl = LIST0 gmatch_hyp_pattern SEP ","; "|-"; p = match_pattern; "]" ->
+        { CAst.make ~loc @@ {
+          q_goal_match_concl = p;
+          q_goal_match_hyps = hl;
+        } }
+    ] ]
+  ;
+  gmatch_rule:
+    [ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
+        { CAst.make ~loc @@ (mp, tac) }
+    ] ]
+  ;
+  gmatch_list:
+    [ [ mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl }
+      | "|"; mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
+  ;
+  q_goal_matching:
+    [ [ m = gmatch_list -> { m } ] ]
+  ;
+  move_location:
+    [ [ "at"; IDENT "top" -> { CAst.make ~loc @@ QMoveFirst }
+      | "at"; IDENT "bottom" -> { CAst.make ~loc @@ QMoveLast }
+      | IDENT "after"; id = ident_or_anti -> { CAst.make ~loc @@ QMoveAfter id }
+      | IDENT "before"; id = ident_or_anti -> { CAst.make ~loc @@ QMoveBefore id }
+    ] ]
+  ;
+  q_move_location:
+    [ [ mv = move_location -> { mv } ] ]
+  ;
+  as_name:
+    [ [ -> { None }
+      | "as"; id = ident_or_anti -> { Some id }
+    ] ]
+  ;
+  pose:
+    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+        { CAst.make ~loc (Some id, c) }
+      | c = Constr.constr; na = as_name -> { CAst.make ~loc (na, c) }
+    ] ]
+  ;
+  q_pose:
+    [ [ p = pose -> { p } ] ]
+  ;
+  as_ipat:
+    [ [ "as"; ipat = simple_intropattern -> { Some ipat }
+      | -> { None }
+    ] ]
+  ;
+  by_tactic:
+    [ [ "by"; tac = tac2expr -> { Some tac }
+      | -> { None }
+    ] ]
+  ;
+  assertion:
+    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+        { CAst.make ~loc (QAssertValue (id, c)) }
+      | test_lpar_id_colon; "("; id = ident_or_anti; ":"; c = Constr.lconstr; ")"; tac = by_tactic ->
+      { let ipat = CAst.make ~loc @@ QIntroNaming (CAst.make ~loc @@ QIntroIdentifier id) in
+        CAst.make ~loc (QAssertType (Some ipat, c, tac)) }
+      | c = Constr.constr; ipat = as_ipat; tac = by_tactic ->
+        { CAst.make ~loc (QAssertType (ipat, c, tac)) }
+    ] ]
+  ;
+  q_assert:
+    [ [ a = assertion -> { a } ] ]
+  ;
+END
+
+(** Extension of constr syntax *)
+
+(*
+GRAMMAR EXTEND Gram
+  Pcoq.Constr.operconstr: LEVEL "0"
+    [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
+      { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
+      | test_ampersand_ident; "&"; id = Prim.ident ->
+      { let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
+        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
+      | test_dollar_ident; "$"; id = Prim.ident ->
+      { let id = Loc.tag ~loc id in
+        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
+        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
+    ] ]
+  ;
+END
+*)
+{
+
+let () =
+
+let open Extend in
+let open Tok in
+let (++) r s = Next (r, s) in
+let rules = [
+  Rule (
+    Stop ++ Aentry test_dollar_ident ++ Atoken (KEYWORD "$") ++ Aentry Prim.ident,
+    begin fun id _ _ loc ->
+      let id = Loc.tag ~loc id in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
+      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
+    end
+  );
+
+  Rule (
+    Stop ++ Aentry test_ampersand_ident ++ Atoken (KEYWORD "&") ++ Aentry Prim.ident,
+    begin fun id _ _ loc ->
+      let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
+    end
+  );
+
+  Rule (
+    Stop ++ Atoken (IDENT "ltac2") ++ Atoken (KEYWORD ":") ++
+      Atoken (KEYWORD "(") ++ Aentry tac2expr ++ Atoken (KEYWORD ")"),
+    begin fun _ tac _ _ _ loc ->
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
+    end
+  )
+] in
+
+Hook.set Tac2entries.register_constr_quotations begin fun () ->
+  Gram.gram_extend Pcoq.Constr.operconstr (Some (Level "0"), [(None, None, rules)])
+end
+
+}
+
+{
+
+let pr_ltac2entry _ = mt () (** FIXME *)
+let pr_ltac2expr _ = mt () (** FIXME *)
+
+}
+
+VERNAC ARGUMENT EXTEND ltac2_entry
+PRINTED BY { pr_ltac2entry }
+| [ tac2def_val(v) ] -> { v }
+| [ tac2def_typ(t) ] -> { t }
+| [ tac2def_ext(e) ] -> { e }
+| [ tac2def_syn(e) ] -> { e }
+| [ tac2def_mut(e) ] -> { e }
+| [ tac2def_run(e) ] -> { e }
+END
+
+{
+
+let classify_ltac2 = function
+| StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
+| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff
+
+}
+
+VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
+| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+    Tac2entries.register_struct ?local e
+  }
+END
+
+{
+
+let _ =
+  let mode = {
+    Proof_global.name = "Ltac2";
+    set = (fun () -> Pvernac.set_command_entry tac2mode);
+    reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode));
+  } in
+  Proof_global.register_proof_mode mode
+
+}
+
+VERNAC ARGUMENT EXTEND ltac2_expr
+PRINTED BY { pr_ltac2expr }
+| [ tac2expr(e) ] -> { e }
+END
+
+{
+
+open G_ltac
+open Vernac_classifier
+
+}
+
+VERNAC { tac2mode } EXTEND VernacLtac2
+| [ ltac2_expr(t) ltac_use_default(default) ] =>
+    { classify_as_proofstep } -> {
+(*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
+    Tac2entries.call ~default t
+  }
+END
+
+{
+
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
+| [ "Print" "Ltac2" reference(tac) ] -> { Tac2entries.print_ltac tac }
+END