Port remaining EXTEND ml4 files to coqpp.

Almost all of ml4 were removed in the process. The only remaining files
are in the test-suite and probably need a bit of fiddling with coq_makefile,
and there only two really remaning ml4 files containing code.

8 files changed, 892 insertions, 638 deletions

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.mlg
index 4de27e8138..c4c4e51ecc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Pp
 open Stdarg
 open Tacarg
@@ -61,22 +63,29 @@ let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
   | false -> Pp.str " <-"
 
-ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
-| [ "->" ] -> [ true ]
-| [ "<-" ] -> [ false ]
-| [ ] -> [ true ]
+}
+
+ARGUMENT EXTEND orient TYPED AS bool PRINTED BY { pr_orient }
+| [ "->" ] -> { true }
+| [ "<-" ] -> { false }
+| [ ] -> { true }
 END
 
+{
+
 let pr_int _ _ _ i = Pp.int i
 
 let _natural = Pcoq.Prim.natural
 
-ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int
-| [ _natural(i) ] -> [ i ]
+}
+
+ARGUMENT EXTEND natural TYPED AS int PRINTED BY { pr_int }
+| [ _natural(i) ] -> { i }
 END
 
-let pr_orient = pr_orient () () ()
+{
 
+let pr_orient = pr_orient () () ()
 
 let pr_int_list = Pp.pr_sequence Pp.int
 let pr_int_list_full _prc _prlc _prt l = pr_int_list l
@@ -115,21 +124,25 @@ let glob_occs ist l = l
 
 let subst_occs evm l = l
 
+}
+
 ARGUMENT EXTEND occurrences
   TYPED AS int list
-  PRINTED BY pr_int_list_full
+  PRINTED BY { pr_int_list_full }
 
-  INTERPRETED BY interp_occs
-  GLOBALIZED BY glob_occs
-  SUBSTITUTED BY subst_occs
+  INTERPRETED BY { interp_occs }
+  GLOBALIZED BY { glob_occs }
+  SUBSTITUTED BY { subst_occs }
 
-  RAW_PRINTED BY pr_occurrences
-  GLOB_PRINTED BY pr_occurrences
+  RAW_PRINTED BY { pr_occurrences }
+  GLOB_PRINTED BY { pr_occurrences }
 
-| [ ne_integer_list(l) ] -> [ ArgArg l ]
-| [ var(id) ] -> [ ArgVar id ]
+| [ ne_integer_list(l) ] -> { ArgArg l }
+| [ var(id) ] -> { ArgVar id }
 END
 
+{
+
 let pr_occurrences = pr_occurrences () () ()
 
 let pr_gen prc _prlc _prtac c = prc c
@@ -146,49 +159,61 @@ let pr_lconstr _ prc _ c = prc c
 
 let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
+}
+
 ARGUMENT EXTEND glob
-    PRINTED BY pr_globc
+    PRINTED BY { pr_globc }
 
-     INTERPRETED BY interp_glob
-     GLOBALIZED BY glob_glob
-     SUBSTITUTED BY subst_glob
+     INTERPRETED BY { interp_glob }
+     GLOBALIZED BY { glob_glob }
+     SUBSTITUTED BY { subst_glob }
 
-     RAW_PRINTED BY pr_gen
-     GLOB_PRINTED BY pr_gen
-  [ constr(c) ] -> [ c ]
+     RAW_PRINTED BY { pr_gen }
+     GLOB_PRINTED BY { pr_gen }
+| [ constr(c) ] -> { c }
 END
 
+{
+
 let l_constr = Pcoq.Constr.lconstr
 
+}
+
 ARGUMENT EXTEND lconstr
     TYPED AS constr
-    PRINTED BY pr_lconstr
-  [ l_constr(c) ] -> [ c ]
+    PRINTED BY { pr_lconstr }
+| [ l_constr(c) ] -> { c }
 END
 
 ARGUMENT EXTEND lglob
   TYPED AS glob
-    PRINTED BY pr_globc
+    PRINTED BY { pr_globc }
 
-     INTERPRETED BY interp_glob
-     GLOBALIZED BY glob_glob
-     SUBSTITUTED BY subst_glob
+     INTERPRETED BY { interp_glob }
+     GLOBALIZED BY { glob_glob }
+     SUBSTITUTED BY { subst_glob }
 
-     RAW_PRINTED BY pr_gen
-     GLOB_PRINTED BY pr_gen
-  [ lconstr(c) ] -> [ c ]
+     RAW_PRINTED BY { pr_gen }
+     GLOB_PRINTED BY { pr_gen }
+| [ lconstr(c) ] -> { c }
 END
 
+{
+
 let interp_casted_constr ist gl c =
   interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
 
+}
+
 ARGUMENT EXTEND casted_constr
   TYPED AS constr
-  PRINTED BY pr_gen
-  INTERPRETED BY interp_casted_constr
-  [ constr(c) ] -> [ c ]
+  PRINTED BY { pr_gen }
+  INTERPRETED BY { interp_casted_constr }
+| [ constr(c) ] -> { c }
 END
 
+{
+
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
 type loc_place = lident gen_place
@@ -227,68 +252,84 @@ let warn_deprecated_instantiate_syntax =
              ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".")
          )
 
+}
+
 ARGUMENT EXTEND hloc
-    PRINTED BY pr_place
-    INTERPRETED BY interp_place
-    GLOBALIZED BY intern_place
-    SUBSTITUTED BY subst_place
-    RAW_PRINTED BY pr_loc_place
-    GLOB_PRINTED BY pr_loc_place
-  [ ] ->
-    [ ConclLocation () ]
+    PRINTED BY { pr_place }
+    INTERPRETED BY { interp_place }
+    GLOBALIZED BY { intern_place }
+    SUBSTITUTED BY { subst_place }
+    RAW_PRINTED BY { pr_loc_place }
+    GLOB_PRINTED BY { pr_loc_place }
+| [ ] ->
+    { ConclLocation () }
   |  [ "in" "|-" "*" ] ->
-    [ ConclLocation () ]
+    { ConclLocation () }
 | [ "in" ident(id) ] ->
-    [ HypLocation ((CAst.make id),InHyp) ]
+    { HypLocation ((CAst.make id),InHyp) }
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ warn_deprecated_instantiate_syntax ("Type","type",id);
-      HypLocation ((CAst.make id),InHypTypeOnly) ]
+    { warn_deprecated_instantiate_syntax ("Type","type",id);
+      HypLocation ((CAst.make id),InHypTypeOnly) }
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
-    [ warn_deprecated_instantiate_syntax ("Value","value",id);
-      HypLocation ((CAst.make id),InHypValueOnly) ]
+    { warn_deprecated_instantiate_syntax ("Value","value",id);
+      HypLocation ((CAst.make id),InHypValueOnly) }
 | [ "in" "(" "type" "of" ident(id) ")" ] ->
-    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
+    { HypLocation ((CAst.make id),InHypTypeOnly) }
 | [ "in" "(" "value" "of" ident(id) ")" ] ->
-    [ HypLocation ((CAst.make id),InHypValueOnly) ]
+    { HypLocation ((CAst.make id),InHypValueOnly) }
 
  END
 
+{
+
 let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m
 
+}
+
 ARGUMENT EXTEND rename
-  TYPED AS ident * ident
-  PRINTED BY pr_rename
-| [ ident(n) "into" ident(m) ] -> [ (n, m) ]
+  TYPED AS (ident * ident)
+  PRINTED BY { pr_rename }
+| [ ident(n) "into" ident(m) ] -> { (n, m) }
 END
 
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
+{
+
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
     | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
+}
+
 ARGUMENT EXTEND by_arg_tac
-  TYPED AS tactic_opt
-  PRINTED BY pr_by_arg_tac
-| [ "by" tactic3(c) ] -> [ Some c ]
-| [ ] -> [ None ]
+  TYPED AS tactic option
+  PRINTED BY { pr_by_arg_tac }
+| [ "by" tactic3(c) ] -> { Some c }
+| [ ] -> { None }
 END
 
+{
+
 let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
 
 let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
 let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
 let in_clause' = Pltac.in_clause
 
+}
+
 ARGUMENT EXTEND in_clause
   TYPED AS clause_dft_concl
-  PRINTED BY pr_in_top_clause
-  RAW_PRINTED BY pr_in_clause
-  GLOB_PRINTED BY pr_in_clause
-| [ in_clause'(cl) ] -> [ cl ]
+  PRINTED BY { pr_in_top_clause }
+  RAW_PRINTED BY { pr_in_clause }
+  GLOB_PRINTED BY { pr_in_clause }
+| [ in_clause'(cl) ] -> { cl }
 END
 
+{
+
 let local_test_lpar_id_colon =
   let err () = raise Stream.Failure in
   Pcoq.Gram.Entry.of_parser "lpar_id_colon"
@@ -305,6 +346,8 @@ let local_test_lpar_id_colon =
 
 let pr_lpar_id_colon _ _ _ _ = mt ()
 
-ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon
-| [ local_test_lpar_id_colon(x) ] -> [ () ]
+}
+
+ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon }
+| [ local_test_lpar_id_colon(x) ] -> { () }
 END
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.mlg
index e5b032e638..b660865e8b 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Pp
 open Constr
 open Genarg
@@ -30,8 +32,14 @@ open Tactics
 open Proofview.Notations
 open Vernacinterp
 
+let wit_hyp = wit_var
+
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
+{
+
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
 (* cutrewrite, dependent rewrite                                      *)
@@ -43,7 +51,7 @@ let with_delayed_uconstr ist c tac =
     use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
-  } in
+ } in
   let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
@@ -54,26 +62,30 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
+}
+
 TACTIC EXTEND replace
-   ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
+| ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
+-> { replace_in_clause_maybe_by ist c1 c2 cl tac }
 END
 
 TACTIC EXTEND replace_term_left
-  [ "replace"  "->" uconstr(c) clause(cl) ]
-  -> [ replace_term ist (Some true) c cl ]
+| [ "replace"  "->" uconstr(c) clause(cl) ]
+  -> { replace_term ist (Some true) c cl }
 END
 
 TACTIC EXTEND replace_term_right
-  [ "replace"  "<-" uconstr(c) clause(cl) ]
-  -> [ replace_term ist (Some false) c cl ]
+| [ "replace"  "<-" uconstr(c) clause(cl) ]
+  -> { replace_term ist (Some false) c cl }
 END
 
 TACTIC EXTEND replace_term
-  [ "replace" uconstr(c) clause(cl) ]
-  -> [ replace_term ist None c cl ]
+| [ "replace" uconstr(c) clause(cl) ]
+  -> { replace_term ist None c cl }
 END
 
+{
+
 let induction_arg_of_quantified_hyp = function
   | AnonHyp n -> None,ElimOnAnonHyp n
   | NamedHyp id -> None,ElimOnIdent (CAst.make id)
@@ -94,28 +106,36 @@ let elimOnConstrWithHoles tac with_evars c =
   Tacticals.New.tclDELAYEDWITHHOLES with_evars c
     (fun c -> tac with_evars (Some (None,ElimOnConstr c)))
 
+}
+
 TACTIC EXTEND simplify_eq
-  [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
+| [ "simplify_eq" ] -> { dEq ~keep_proofs:None false None }
+| [ "simplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) false c }
 END
 TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
+| [ "esimplify_eq" ] -> { dEq ~keep_proofs:None true None }
+| [ "esimplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) true c }
 END
 
+{
+
 let discr_main c = elimOnConstrWithHoles discr_tac false c
 
+}
+
 TACTIC EXTEND discriminate
-| [ "discriminate" ] -> [ discr_tac false None ]
+| [ "discriminate" ] -> { discr_tac false None }
 | [ "discriminate" destruction_arg(c) ] ->
-    [ mytclWithHoles discr_tac false c ]
+    { mytclWithHoles discr_tac false c }
 END
 TACTIC EXTEND ediscriminate
-| [ "ediscriminate" ] -> [ discr_tac true None ]
+| [ "ediscriminate" ] -> { discr_tac true None }
 | [ "ediscriminate" destruction_arg(c) ] ->
-    [ mytclWithHoles discr_tac true c ]
+    { mytclWithHoles discr_tac true c }
 END
 
+{
+
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
   discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
@@ -123,39 +143,45 @@ let discrHyp id =
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None None) with_evars c
 
+}
+
 TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
+| [ "injection" ] -> { injClause None None false None }
+| [ "injection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) false c }
 END
 TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
+| [ "einjection" ] -> { injClause None None true None }
+| [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c }
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" intropattern_list(ipat)] ->
-    [ injClause None (Some ipat) false None ]
+    { injClause None (Some ipat) false None }
 | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    [ mytclWithHoles (injClause None (Some ipat)) false c ]
+    { mytclWithHoles (injClause None (Some ipat)) false c }
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" intropattern_list(ipat)] ->
-    [ injClause None (Some ipat) true None ]
+    { injClause None (Some ipat) true None }
 | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    [ mytclWithHoles (injClause None (Some ipat)) true c ]
+    { mytclWithHoles (injClause None (Some ipat)) true c }
 END
 TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
+| [ "simple" "injection" ] -> { simpleInjClause None false None }
+| [ "simple" "injection" destruction_arg(c) ] -> { mytclWithHoles (simpleInjClause None) false c }
 END
 
+{
+
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
   injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
 
+}
+
 TACTIC EXTEND dependent_rewrite
-| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> { rewriteInConcl b c }
 | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
-    -> [ rewriteInHyp b c id ]
+    -> { rewriteInHyp b c id }
 END
 
 (** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
@@ -163,43 +189,53 @@ END
     "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
 
 TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
 | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
-    -> [ cutRewriteInHyp b eqn id ]
+    -> { cutRewriteInHyp b eqn id }
 END
 
 (**********************************************************************)
 (* Decompose                                                          *)
 
 TACTIC EXTEND decompose_sum
-| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ]
+| [ "decompose" "sum" constr(c) ] -> { Elim.h_decompose_or c }
 END
 
 TACTIC EXTEND decompose_record
-| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ]
+| [ "decompose" "record" constr(c) ] -> { Elim.h_decompose_and c }
 END
 
 (**********************************************************************)
 (* Contradiction                                                      *)
 
+{
+
 open Contradiction
 
+}
+
 TACTIC EXTEND absurd
- [ "absurd" constr(c) ] -> [ absurd c ]
+| [ "absurd" constr(c) ] -> { absurd c }
 END
 
+{
+
 let onSomeWithHoles tac = function
   | None -> tac None
   | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
 
+}
+
 TACTIC EXTEND contradiction
- [ "contradiction" constr_with_bindings_opt(c) ] ->
-    [ onSomeWithHoles contradiction c ]
+| [ "contradiction" constr_with_bindings_opt(c) ] ->
+    { onSomeWithHoles contradiction c }
 END
 
 (**********************************************************************)
 (* AutoRewrite                                                        *)
 
+{
+
 open Autorewrite
 
 let pr_orient _prc _prlc _prt = function
@@ -209,50 +245,58 @@ let pr_orient _prc _prlc _prt = function
 let pr_orient_string _prc _prlc _prt (orient, s) =
   pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s
 
-ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string
-| [ orient(r) preident(i) ] -> [ r, i ]
+}
+
+ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string }
+| [ orient(r) preident(i) ] -> { r, i }
 END
 
 TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] ->
-    [ auto_multi_rewrite  l ( cl) ]
+    { auto_multi_rewrite  l ( cl) }
 | [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
-    [
+    {
       auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
-    ]
+   }
 END
 
 TACTIC EXTEND autorewrite_star
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
-    [ auto_multi_rewrite ~conds:AllMatches l cl ]
+    { auto_multi_rewrite ~conds:AllMatches l cl }
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
-  [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ]
+  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl }
 END
 
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
+{
+
 let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
   let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
   with_delayed_uconstr ist c
     (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
 
+}
+
 TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
-    [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ]
+    { rewrite_star ist (Some id) o (occurrences_of occ) c tac }
 | [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ]
+    { rewrite_star ist (Some id) o (occurrences_of occ) c tac }
 | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star ist (Some id) o Locus.AllOccurrences c tac ]
+    { rewrite_star ist (Some id) o Locus.AllOccurrences c tac }
 | [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
-    [ rewrite_star ist None o (occurrences_of occ) c tac ]
+    { rewrite_star ist None o (occurrences_of occ) c tac }
 | [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] ->
-    [ rewrite_star ist None o Locus.AllOccurrences c tac ]
+    { rewrite_star ist None o Locus.AllOccurrences c tac }
     END
 
 (**********************************************************************)
 (* Hint Rewrite                                                       *)
 
+{
+
 let add_rewrite_hint ~poly bases ort t lcsr =
   let env = Global.env() in
   let sigma = Evd.from_env env in
@@ -274,21 +318,25 @@ let add_rewrite_hint ~poly bases ort t lcsr =
 
 let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
 
-VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint
-  [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ]
+}
+
+VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+  { add_rewrite_hint ~poly:atts.polymorphic bl o None l }
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident_list(bl) ] ->
-  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ]
+  { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l }
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ]
+  { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l }
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ]
+  { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l }
 END
 
 (**********************************************************************)
 (* Refine                                                             *)
 
+{
+
 open EConstr
 open Vars
 
@@ -304,7 +352,7 @@ let refine_tac ist simple with_classes c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
-      { constr_flags () with Pretyping.use_typeclasses = with_classes } in
+      { (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
     let update = begin fun sigma ->
@@ -317,125 +365,141 @@ let refine_tac ist simple with_classes c =
            Proofview.shelve_unifiable
   end
 
+}
+
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] ->
-   [ refine_tac ist false true c ]
+   { refine_tac ist false true c }
 END
 
 TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] ->
-   [ refine_tac ist true true c ]
+   { refine_tac ist true true c }
 END
 
 TACTIC EXTEND notcs_refine
 | [ "notypeclasses" "refine" uconstr(c) ] ->
-   [ refine_tac ist false false c ]
+   { refine_tac ist false false c }
 END
 
 TACTIC EXTEND notcs_simple_refine
 | [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
-   [ refine_tac ist true false c ]
+   { refine_tac ist true false c }
 END
 
 (* Solve unification constraints using heuristics or fail if any remain *)
 TACTIC EXTEND solve_constraints
-[ "solve_constraints" ] -> [ Refine.solve_constraints ]
+| [ "solve_constraints" ] -> { Refine.solve_constraints }
 END
 
 (**********************************************************************)
 (* Inversion lemmas (Leminv)                                          *)
 
+{
+
 open Inv
 open Leminv
 
 let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 
+}
+
 (*VERNAC ARGUMENT EXTEND sort_family
-| [ "Set" ] -> [ InSet ]
-| [ "Prop" ] -> [ InProp ]
-| [ "Type" ] -> [ InType ]
+| [ "Set" ] -> { InSet }
+| [ "Prop" ] -> { InProp }
+| [ "Type" ] -> { InType }
 END*)
 
-VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear
+VERNAC COMMAND EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
-  => [ seff na ]
-  -> [ fun ~atts ~st ->
+  => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac }
 
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ fun ~atts ~st ->
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion
+VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
-  => [ seff na ]
-  -> [ fun ~atts ~st ->
+  => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac }
 
-| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
-  -> [ fun ~atts ~st ->
+| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion
+VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
-  => [ seff na ]
-  -> [  fun ~atts ~st ->
+  => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear
+VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
-  => [ seff na ]
-  -> [  fun ~atts ~st ->
+  => { seff na }
+  -> {
       let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ]
+      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
 END
 
 (**********************************************************************)
 (* Subst                                                              *)
 
 TACTIC EXTEND subst
-| [ "subst" ne_var_list(l) ] -> [ subst l ]
-| [ "subst" ] -> [ subst_all () ]
+| [ "subst" ne_var_list(l) ] -> { subst l }
+| [ "subst" ] -> { subst_all () }
 END
 
+{
+
 let simple_subst_tactic_flags =
   { only_leibniz = true; rewrite_dependent_proof = false }
 
+}
+
 TACTIC EXTEND simple_subst
-| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags () ]
+| [ "simple" "subst" ] -> { subst_all ~flags:simple_subst_tactic_flags () }
 END
 
+{
+
 open Evar_tactics
 
+}
+
 (**********************************************************************)
 (* Evar creation                                                      *)
 
 (* TODO: add support for some test similar to g_constr.name_colon so that
    expressions like "evar (list A)" do not raise a syntax error *)
 TACTIC EXTEND evar
-  [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ]
-| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ]
+| [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> { let_evar (Name.Name id) typ }
+| [ "evar" constr(typ) ] -> { let_evar Name.Anonymous typ }
 END
 
 TACTIC EXTEND instantiate
-  [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
-    [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ]
+| [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
+    { Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals }
 | [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] ->
-    [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ]
-| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ]
+    { Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals }
+| [ "instantiate" ] -> { Proofview.V82.nf_evar_goals }
 END
 
 (**********************************************************************)
 (** Nijmegen "step" tactic for setoid rewriting                       *)
 
+{
+
 open Tactics
 open Glob_term
 open Libobject
@@ -489,28 +553,32 @@ let add_transitivity_lemma left lem =
   let lem' = EConstr.to_constr sigma lem' in
   add_anonymous_leaf (inTransitivity (left,lem'))
 
+}
+
 (* Vernacular syntax *)
 
 TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ]
-| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ]
+| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) }
+| ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) }
 END
 
 TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ]
-| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ]
+| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) }
+| ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) }
 END
 
 VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF
 | [ "Declare" "Left" "Step" constr(t) ] ->
-    [ add_transitivity_lemma true t ]
+    { add_transitivity_lemma true t }
 END
 
 VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
 | [ "Declare" "Right" "Step" constr(t) ] ->
-    [ add_transitivity_lemma false t ]
+    { add_transitivity_lemma false t }
 END
 
+{
+
 let cache_implicit_tactic (_,tac) = match tac with
   | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac)
   | None -> Pfedit.clear_implicit_tactic ()
@@ -537,9 +605,11 @@ let clear_implicit_tactic () =
   let () = warn_deprecated_implicit_tactic () in
   Lib.add_anonymous_leaf (inImplicitTactic None)
 
+}
+
 VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
-| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ]
-| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ]
+| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac }
+| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () }
 END
 
 
@@ -549,16 +619,16 @@ END
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ]
+| ["generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false id }
 END
 TACTIC EXTEND dep_generalize_eqs
-| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ]
+| ["dependent" "generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false ~force_dep:true id }
 END
 TACTIC EXTEND generalize_eqs_vars
-| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ]
+| ["generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~generalize_vars:true id }
 END
 TACTIC EXTEND dep_generalize_eqs_vars
-| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ]
+| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id }
 END
 
 (** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] 
@@ -566,7 +636,7 @@ END
     during dependent induction. For internal use. *)
 
 TACTIC EXTEND specialize_eqs
-[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
+| [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id }
 END
 
 (**********************************************************************)
@@ -577,6 +647,8 @@ END
 (* Contributed by Chung-Kil Hur (Winter 2009)                         *)
 (**********************************************************************)
 
+{
+
 let subst_var_with_hole occ tid t = 
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
@@ -593,7 +665,7 @@ let subst_var_with_hole occ tid t =
                   Evar_kinds.qm_obligation=Evar_kinds.Define true;
                   Evar_kinds.qm_name=Anonymous;
                   Evar_kinds.qm_record_field=None;
-              }, IntroAnonymous, None)))
+             }, IntroAnonymous, None)))
         else x
     | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
@@ -608,7 +680,7 @@ let subst_hole_with_term occ tc t =
                 Evar_kinds.qm_obligation=Evar_kinds.Define true;
                 Evar_kinds.qm_name=Anonymous;
                 Evar_kinds.qm_record_field=None;
-            }, IntroAnonymous, s) ->
+           }, IntroAnonymous, s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
@@ -618,7 +690,7 @@ let subst_hole_with_term occ tc t =
                Evar_kinds.qm_obligation=Evar_kinds.Define true;
                Evar_kinds.qm_name=Anonymous;
                Evar_kinds.qm_record_field=None;
-           },IntroAnonymous,s))
+          },IntroAnonymous,s))
     | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
@@ -659,9 +731,11 @@ let hResolve_auto id c t =
   in
   resolve_auto 1
 
+}
+
 TACTIC EXTEND hresolve_core
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c occ t ]
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t }
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t }
 END
 
 (**
@@ -669,7 +743,7 @@ END
 *)
 
 TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ]
+| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n }
 END
 
 (**********************************************************************)
@@ -682,6 +756,8 @@ END
 (* Contributed by Julien Forest and Pierre Courtieu (july 2010)       *)
 (**********************************************************************)
 
+{
+
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
@@ -763,9 +839,11 @@ let destauto_in id =
   destauto ctype
   end
 
+}
+
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ]
-| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
+| [ "destauto" ] -> { Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end }
+| [ "destauto" "in" hyp(id) ] -> { destauto_in id }
 END
 
 (**********************************************************************)
@@ -776,116 +854,116 @@ END
 (**********************************************************************)
 
 TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl ->
-      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl ->
-      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
+| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end }
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end }
 END
 
 (* ********************************************************************* *)
 
 TACTIC EXTEND constr_eq
-| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ]
+| [ "constr_eq" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:false x y }
 END
 
 TACTIC EXTEND constr_eq_strict
-| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ]
+| [ "constr_eq_strict" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:true x y }
 END
 
 TACTIC EXTEND constr_eq_nounivs
-| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [
+| [ "constr_eq_nounivs" constr(x) constr(y) ] -> {
     Proofview.tclEVARMAP >>= fun sigma ->
-    if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
+    if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") }
 END
 
 TACTIC EXTEND is_evar
-| [ "is_evar" constr(x) ] -> [
+| [ "is_evar" constr(x) ] -> {
     Proofview.tclEVARMAP >>= fun sigma ->
     match EConstr.kind sigma x with
       | Evar _ -> Proofview.tclUNIT ()
       | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
-    ]
+   }
 END
 
 TACTIC EXTEND has_evar
-| [ "has_evar" constr(x) ] -> [
+| [ "has_evar" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   if Evarutil.has_undefined_evars sigma x
   then Proofview.tclUNIT ()
   else Tacticals.New.tclFAIL 0 (str "No evars")
-]
+}
 END
 
 TACTIC EXTEND is_hyp
-| [ "is_var" constr(x) ] -> [
+| [ "is_var" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Var _ ->  Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ]
+    | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") }
 END
 
 TACTIC EXTEND is_fix
-| [ "is_fix" constr(x) ] -> [
+| [ "is_fix" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Fix _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") }
+END
 
 TACTIC EXTEND is_cofix
-| [ "is_cofix" constr(x) ] -> [
+| [ "is_cofix" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | CoFix _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") }
+END
 
 TACTIC EXTEND is_ind
-| [ "is_ind" constr(x) ] -> [
+| [ "is_ind" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Ind _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") }
+END
 
 TACTIC EXTEND is_constructor
-| [ "is_constructor" constr(x) ] -> [
+| [ "is_constructor" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Construct _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") }
+END
 
 TACTIC EXTEND is_proj
-| [ "is_proj" constr(x) ] -> [
+| [ "is_proj" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Proj _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") }
+END
 
 TACTIC EXTEND is_const
-| [ "is_const" constr(x) ] -> [
+| [ "is_const" constr(x) ] -> {
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
     | Const _ -> Proofview.tclUNIT ()
-    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ]
-END;;
+    | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") }
+END
 
 (* Command to grab the evars left unresolved at the end of a proof. *)
 (* spiwack: I put it in extratactics because it is somewhat tied with
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
-[ "Grab" "Existential" "Variables" ]
-  => [ Vernac_classifier.classify_as_proofstep ]
-  -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
+| [ "Grab" "Existential" "Variables" ]
+  => { Vernac_classifier.classify_as_proofstep }
+  -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) }
 END
 
 (* Shelves all the goals under focus. *)
 TACTIC EXTEND shelve
 | [ "shelve" ] ->
-    [ Proofview.shelve ]
+    { Proofview.shelve }
 END
 
 (* Shelves the unifiable goals under focus, i.e. the goals which
@@ -893,25 +971,25 @@ END
    considered). *)
 TACTIC EXTEND shelve_unifiable
 | [ "shelve_unifiable" ] ->
-    [ Proofview.shelve_unifiable ]
+    { Proofview.shelve_unifiable }
 END
 
 (* Unshelves the goal shelved by the tactic. *)
 TACTIC EXTEND unshelve
 | [ "unshelve" tactic1(t) ] ->
-    [
+    {
       Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
       let gls = List.map Proofview.with_empty_state gls in
       Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
       Proofview.Unsafe.tclSETGOALS (gls @ ogls)
-    ]
+   }
 END
 
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
-[ "Unshelve" ]
-  => [ Vernac_classifier.classify_as_proofstep ]
-  -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) ]
+| [ "Unshelve" ]
+  => { Vernac_classifier.classify_as_proofstep }
+  -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -919,24 +997,26 @@ END
    these goals. *)
 TACTIC EXTEND give_up
 | [ "give_up" ] ->
-    [ Proofview.give_up ]
+    { Proofview.give_up }
 END
 
 (* cycles [n] goals *)
 TACTIC EXTEND cycle
-| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle n ]
+| [ "cycle" int_or_var(n) ] -> { Proofview.cycle n }
 END
 
 (* swaps goals number [i] and [j] *)
 TACTIC EXTEND swap
-| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap i j ]
+| [ "swap" int_or_var(i) int_or_var(j) ] -> { Proofview.swap i j }
 END
 
 (* reverses the list of focused goals *)
 TACTIC EXTEND revgoals
-| [ "revgoals" ] -> [ Proofview.revgoals ]
+| [ "revgoals" ] -> { Proofview.revgoals }
 END
 
+{
+
 type cmp =
   | Eq
   | Lt | Le
@@ -965,29 +1045,35 @@ let pr_itest = pr_test_gen Pp.int
 
 let pr_itest' _prc _prlc _prt = pr_itest
 
+}
 
-
-ARGUMENT EXTEND comparison PRINTED BY pr_cmp'
-| [ "="  ] -> [ Eq ]
-| [ "<"  ] -> [ Lt ]
-| [ "<=" ] -> [ Le ]
-| [ ">"  ] -> [ Gt ]
-| [ ">=" ] -> [ Ge ]
+ARGUMENT EXTEND comparison PRINTED BY { pr_cmp' }
+| [ "="  ] -> { Eq }
+| [ "<"  ] -> { Lt }
+| [ "<=" ] -> { Le }
+| [ ">"  ] -> { Gt }
+| [ ">=" ] -> { Ge }
     END
 
+{
+
 let interp_test ist gls = function
   | Test (c,x,y) ->
       project gls ,
       Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y)
 
+}
+
 ARGUMENT EXTEND test
-  PRINTED BY pr_itest'
-  INTERPRETED BY interp_test
-  RAW_PRINTED BY pr_test'
-  GLOB_PRINTED BY pr_test'
-| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ]
+  PRINTED BY { pr_itest' }
+  INTERPRETED BY { interp_test }
+  RAW_PRINTED BY { pr_test' }
+  GLOB_PRINTED BY { pr_test' }
+| [ int_or_var(x) comparison(c) int_or_var(y) ] -> { Test(c,x,y) }
 END
 
+{
+
 let interp_cmp = function
   | Eq -> Int.equal
   | Lt -> ((<):int->int->bool)
@@ -1005,11 +1091,14 @@ let guard tst =
     let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
     Tacticals.New.tclZEROMSG msg
 
+}
 
 TACTIC EXTEND guard
-| [ "guard" test(tst) ] -> [ guard tst ]
+| [ "guard" test(tst) ] -> { guard tst }
 END
 
+{
+
 let decompose l c =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
@@ -1021,14 +1110,16 @@ let decompose l c =
     Elim.h_decompose l c
   end
 
+}
+
 TACTIC EXTEND decompose
-| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
+| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> { decompose l c }
 END
 
 (** library/keys *)
 
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
-| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> {
   let get_key c =
     let env = Global.env () in
     let evd = Evd.from_env env in
@@ -1040,26 +1131,30 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
   let k2 = get_key c' in
     match k1, k2 with
     | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
-    | _ -> () ]
+    | _ -> () }
 END
 
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ]
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
 END
 
 
 VERNAC COMMAND EXTEND OptimizeProof
-| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] ->
-  [ Proof_global.compact_the_proof () ]
-| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] ->
-  [ Gc.compact () ]
+| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } ->
+  { Proof_global.compact_the_proof () }
+| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } ->
+  { Gc.compact () }
 END
 
 (** tactic analogous to "OPTIMIZE HEAP" *)
 
+{
+
 let tclOPTIMIZE_HEAP =
   Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))
 
+}
+
 TACTIC EXTEND optimize_heap
-| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ]
+| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP }
 END
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.mlg
index 6913543c9a..c07b653f3a 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Pp
 open Constr
 open Stdarg
@@ -16,29 +18,39 @@ open Pcoq.Constr
 open Pltac
 open Hints
 
+let wit_hyp = wit_var
+
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
 (* Hint bases *)
 
 
 TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ Eauto.e_assumption ]
+| [ "eassumption" ] -> { Eauto.e_assumption }
 END
 
 TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ]
+| [ "eexact" constr(c) ] -> { Eauto.e_give_exact c }
 END
 
+{
+
 let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
 
+}
+
 ARGUMENT EXTEND hintbases
-  TYPED AS preident_list_opt
-  PRINTED BY pr_hintbases
-| [ "with" "*" ] -> [ None ]
-| [ "with" ne_preident_list(l) ] -> [ Some l ]
-| [ ] -> [ Some [] ]
+  TYPED AS preident list option
+  PRINTED BY { pr_hintbases }
+| [ "with" "*" ] -> { None }
+| [ "with" ne_preident_list(l) ] -> { Some l }
+| [ ] -> { Some [] }
 END
 
+{
+
 let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
@@ -58,102 +70,108 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using
     (let sigma, env = Pfedit.get_current_context () in
      Printer.pr_closed_glob_env env sigma)
 
+}
+
 ARGUMENT EXTEND auto_using
-  TYPED AS uconstr_list
-  PRINTED BY pr_auto_using
-  RAW_PRINTED BY pr_auto_using_raw
-  GLOB_PRINTED BY pr_auto_using_glob
-| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
-| [ ] -> [ [] ]
+  TYPED AS uconstr list
+  PRINTED BY { pr_auto_using }
+  RAW_PRINTED BY { pr_auto_using_raw }
+  GLOB_PRINTED BY { pr_auto_using_glob }
+| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l }
+| [ ] -> { [] }
 END
 
 (** Auto *)
 
 TACTIC EXTEND trivial
 | [ "trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial (eval_uconstrs ist lems) db ]
+    { Auto.h_trivial (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_trivial
 | [ "info_trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ]
+    { Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND debug_trivial
 | [ "debug" "trivial" auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ]
+    { Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND auto
 | [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto n (eval_uconstrs ist lems) db ]
+    { Auto.h_auto n (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_auto
 | [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ]
+    { Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND debug_auto
 | [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
-    [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ]
+    { Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db }
 END
 
 (** Eauto *)
 
 TACTIC EXTEND prolog
 | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
-    [ Eauto.prolog_tac (eval_uconstrs ist l) n ]
+    { Eauto.prolog_tac (eval_uconstrs ist l) n }
 END
 
+{
+
 let make_depth n = snd (Eauto.make_dimension n None)
 
+}
+
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ]
+    { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND new_eauto
 | [ "new" "auto" int_or_var_opt(n) auto_using(lems)
     hintbases(db) ] ->
-    [ match db with
+    { match db with
       | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems)
-      | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l ]
+      | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l }
 END
 
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ]
+    { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ]
+    { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND dfs_eauto
 | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
-    [ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db ]
+    { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ]
+| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl }
 END
 
 TACTIC EXTEND autounfold_one
 | [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
-    [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) ]
+    { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) }
 | [ "autounfold_one" hintbases(db) ] ->
-    [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
+    { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None }
       END
 
 TACTIC EXTEND unify
-| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ]
-| ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
+| ["unify" constr(x) constr(y) ] -> { Tactics.unify x y }
+| ["unify" constr(x) constr(y) "with" preident(base)  ] -> {
     let table = try Some (Hints.searchtable_map base) with Not_found -> None in
     match table with
     | None ->
@@ -162,65 +180,70 @@ TACTIC EXTEND unify
     | Some t ->
       let state = Hints.Hint_db.transparent_state t in
       Tactics.unify ~state x y
-  ]
+  }
 END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
 END
 
+{
+
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
 let glob_hints_path_atom ist = Hints.glob_hints_path_atom
 
+}
+
 ARGUMENT EXTEND hints_path_atom
-  PRINTED BY pr_hints_path_atom
+  PRINTED BY { pr_hints_path_atom }
 
-  GLOBALIZED BY glob_hints_path_atom
+  GLOBALIZED BY { glob_hints_path_atom }
 
-  RAW_PRINTED BY pr_pre_hints_path_atom
-  GLOB_PRINTED BY pr_hints_path_atom
-| [ ne_global_list(g) ] -> [ Hints.PathHints g ]
-| [ "_" ] -> [ Hints.PathAny ]
+  RAW_PRINTED BY { pr_pre_hints_path_atom }
+  GLOB_PRINTED BY { pr_hints_path_atom }
+| [ ne_global_list(g) ] -> { Hints.PathHints g }
+| [ "_" ] -> { Hints.PathAny }
 END
 
+{
+
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c
 let glob_hints_path ist = Hints.glob_hints_path
 
+}
+
 ARGUMENT EXTEND hints_path
-PRINTED BY pr_hints_path
+PRINTED BY { pr_hints_path }
 
-GLOBALIZED BY glob_hints_path
-RAW_PRINTED BY pr_pre_hints_path
-GLOB_PRINTED BY pr_hints_path
+GLOBALIZED BY { glob_hints_path }
+RAW_PRINTED BY { pr_pre_hints_path }
+GLOB_PRINTED BY { pr_hints_path }
 
-| [ "(" hints_path(p) ")"  ] -> [ p ]
-| [ hints_path(p) "*" ] -> [ Hints.PathStar p ]
-| [ "emp" ] -> [ Hints.PathEmpty ]
-| [ "eps" ] -> [ Hints.PathEpsilon ]
-| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ]
-| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ]
-| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
+| [ "(" hints_path(p) ")"  ] -> { p }
+| [ hints_path(p) "*" ] -> { Hints.PathStar p }
+| [ "emp" ] -> { Hints.PathEmpty }
+| [ "eps" ] -> { Hints.PathEpsilon }
+| [ hints_path(p) "|" hints_path(q) ] -> { Hints.PathOr (p, q) }
+| [ hints_path_atom(a) ] -> { Hints.PathAtom a }
+| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) }
 END
 
 ARGUMENT EXTEND opthints
-  TYPED AS preident_list_opt
-  PRINTED BY pr_hintbases
-| [ ":" ne_preident_list(l) ] -> [ Some l ]
-| [ ] -> [ None ]
+  TYPED AS preident list option
+  PRINTED BY { pr_hintbases }
+| [ ":" ne_preident_list(l) ] -> { Some l }
+| [ ] -> { None }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
-| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
-    fun ~atts ~st -> begin
+VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
+| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
         let open Vernacinterp in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
         Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
-        st
-      end
- ]
+ }
 END
 
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.mlg
index 265368833b..9ecc36bdf3 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.mlg
@@ -8,85 +8,103 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Class_tactics
 open Stdarg
 open Tacarg
 
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
 (** Options: depth, debug and transparency settings. *)
 
+{
+
 let set_transparency cl b =
   List.iter (fun r ->
     let gr = Smartlocate.global_with_alias r in
     let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
       Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl
 
+}
+
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
-    set_transparency cl true ]
+| [ "Typeclasses" "Transparent" reference_list(cl) ] -> {
+    set_transparency cl true }
 END
 
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
-    set_transparency cl false ]
+| [ "Typeclasses" "Opaque" reference_list(cl) ] -> {
+    set_transparency cl false }
 END
 
+{
+
 let pr_debug _prc _prlc _prt b =
   if b then Pp.str "debug" else Pp.mt()
 
-ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
-| [ "debug" ] -> [ true ]
-| [ ] -> [ false ]
+}
+
+ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug }
+| [ "debug" ] -> { true }
+| [ ] -> { false }
 END
 
+{
+
 let pr_search_strategy _prc _prlc _prt = function
   | Some Dfs -> Pp.str "dfs"
   | Some Bfs -> Pp.str "bfs"
   | None -> Pp.mt ()
 
-ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy
-| [ "(bfs)" ] -> [ Some Bfs ]
-| [ "(dfs)" ] -> [ Some Dfs ]
-| [ ] -> [ None ] 
+}
+
+ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
+| [ "(bfs)" ] -> { Some Bfs }
+| [ "(dfs)" ] -> { Some Dfs }
+| [ ] -> { None }
 END
 
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
      set_typeclasses_debug d;
      Option.iter set_typeclasses_strategy s;
      set_typeclasses_depth depth
-   ]
+   }
 END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
  | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
-    [ typeclasses_eauto ~strategy:Bfs ~depth:d l ]
+    { typeclasses_eauto ~strategy:Bfs ~depth:d l }
  | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
-    [ typeclasses_eauto ~depth:d l ]
- | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
-     typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
+    { typeclasses_eauto ~depth:d l }
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
+     typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] }
 END
 
 TACTIC EXTEND head_of_constr
-  [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ]
+| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c }
 END
 
 TACTIC EXTEND not_evar
-  [ "not_evar" constr(ty) ] -> [ not_evar ty ]
+| [ "not_evar" constr(ty) ] -> { not_evar ty }
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ is_ground ty ]
+| [ "is_ground" constr(ty) ] -> { is_ground ty }
 END
 
 TACTIC EXTEND autoapply
-  [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ]
+| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i }
 END
 
+{
+
 (** TODO: DEPRECATE *)
 (* A progress test that allows to see if the evars have changed *)
 open Constr
@@ -112,6 +130,8 @@ let progress_evars t =
     in t <*> check
   end
 
+}
+
 TACTIC EXTEND progress_evars
-  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
+| [ "progress_evars" tactic(t) ] -> { progress_evars (Tacinterp.tactic_of_value ist t) }
 END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.mlg
index 929390b1c4..d62f985350 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.mlg
@@ -10,6 +10,8 @@
 
 DECLARE PLUGIN "ltac_plugin"
 
+{
+
 open Util
 open Pp
 open Glob_term
@@ -80,282 +82,288 @@ let test_bracket_ident =
 
 let hint = G_proofs.hint
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
           tactic_mode constr_may_eval constr_eval toplevel_selector
           operconstr;
 
   tactic_then_last:
-    [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
-          Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
-      | -> [||]
+    [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" ->
+        { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) }
+      | -> { [||] }
     ] ]
   ;
   tactic_then_gen:
-    [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
-      | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
-      | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
-      | ta = tactic_expr -> ([ta], None)
-      | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
-      | -> ([TacId []], None)
+    [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
+      | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
+      | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) }
+      | ta = tactic_expr -> { ([ta], None) }
+      | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
+      | -> { ([TacId []], None) }
     ] ]
   ;
   tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
                            for [TacExtend] *)
-  [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ]
+  [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
   ;
   tactic_expr:
     [ "5" RIGHTA
-      [ te = binder_tactic -> te ]
+      [ te = binder_tactic -> { te } ]
     | "4" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
-      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1)
-      | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" ->
+      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
+      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
+      | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+          let (first,tail) = tg in
 	  match l , tail with
           | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
 	  | true  , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
           | false , None -> TacThen (ta0,TacDispatch first)
-	  | true  , None -> TacThens (ta0,first) ]
+	  | true  , None -> TacThens (ta0,first) } ]
     | "3" RIGHTA
-      [ IDENT "try"; ta = tactic_expr -> TacTry ta
-      | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
-      | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
-      | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta)
-      | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
-      | IDENT "progress"; ta = tactic_expr -> TacProgress ta
-      | IDENT "once"; ta = tactic_expr -> TacOnce ta
-      | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
-      | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
+      [ IDENT "try"; ta = tactic_expr -> { TacTry ta }
+      | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
+      | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) }
+      | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) }
+      | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta }
+      | IDENT "progress"; ta = tactic_expr -> { TacProgress ta }
+      | IDENT "once"; ta = tactic_expr -> { TacOnce ta }
+      | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta }
+      | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta }
 (*To do: put Abstract in Refiner*)
-      | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
+      | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-          TacAbstract (tc,Some s)
-      | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ]
+        { TacAbstract (tc,Some s) }
+      | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1)
-      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) 
+      [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
+      | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) }
       | IDENT "tryif" ; ta = tactic_expr ;
               "then" ; tat = tactic_expr ;
-              "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae)
-      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
-      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
+              "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) }
+      | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
+      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ]
     | "1" RIGHTA
       [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
-          TacMatchGoal (b,false,mrl)
+          { TacMatchGoal (b,false,mrl) }
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
-          TacMatchGoal (b,true,mrl)
+          { TacMatchGoal (b,true,mrl) }
       |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
-          TacMatch (b,c,mrl)
+          { TacMatch (b,c,mrl) }
       | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-	  TacFirst l
+	  { TacFirst l }
       | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-	  TacSolve l
-      | IDENT "idtac"; l = LIST0 message_token -> TacId l
-      | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ];
-	  l = LIST0 message_token -> TacFail (g,n,l)
-      | st = simple_tactic -> st
-      | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a)
+	  { TacSolve l }
+      | IDENT "idtac"; l = LIST0 message_token -> { TacId l }
+      | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
+	  l = LIST0 message_token -> { TacFail (g,n,l) }
+      | st = simple_tactic -> { st }
+      | a = tactic_arg -> { TacArg(Loc.tag ~loc a) }
       | r = reference; la = LIST0 tactic_arg_compat ->
-          TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ]
+        { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ]
     | "0"
-      [ "("; a = tactic_expr; ")" -> a
-      | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
+      [ "("; a = tactic_expr; ")" -> { a }
+      | "["; ">"; tg = tactic_then_gen; "]" -> {
+          let (tf,tail) = tg in
           begin match tail with
           | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
           | None -> TacDispatch tf
-          end
-      | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ]
+          end }
+      | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ]
   ;
   failkw:
-  [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
+  [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
   ;
   (* binder_tactic: level 5 of tactic_expr *)
   binder_tactic:
     [ RIGHTA
       [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
-          TacFun (it,body)
-      | "let"; isrec = [IDENT "rec" -> true | -> false];
+          { TacFun (it,body) }
+      | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
           llc = LIST1 let_clause SEP "with"; "in";
-          body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body)
-      | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
+          body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) }
+      | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ]
   ;
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
-    [ [ a = tactic_arg -> a
-      | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c))
+    [ [ a = tactic_arg -> { a }
+      | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
       (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
-      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
+      | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
   tactic_arg:
-    [ [ c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
-      | IDENT "type_term"; c=uconstr -> TacPretype c
-      | IDENT "numgoals" -> TacNumgoals ] ]
+    [ [ c = constr_eval -> { ConstrMayEval c }
+      | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l }
+      | IDENT "type_term"; c=uconstr -> { TacPretype c }
+      | IDENT "numgoals" -> { TacNumgoals } ] ]
   ;
   (* If a qualid is given, use its short name. TODO: have the shortest
      non ambiguous name where dots are replaced by "_"? Probably too
      verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
-        | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ]
+    [ [ s = STRING -> { Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) }
+        | qid = qualid -> { Locus.ArgVar (CAst.make ~loc @@ Libnames.qualid_basename qid) } ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-          ConstrEval (rtc,c)
+          { ConstrEval (rtc,c) }
       | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
-          ConstrContext (id,c)
+          { ConstrContext (id,c) }
       | IDENT "type"; IDENT "of"; c = Constr.constr ->
-          ConstrTypeOf c ] ]
+          { ConstrTypeOf c } ] ]
   ;
   constr_may_eval: (* For extensions *)
-    [ [ c = constr_eval -> c
-      | c = Constr.constr -> ConstrTerm c ] ]
+    [ [ c = constr_eval -> { c }
+      | c = Constr.constr -> { ConstrTerm c } ] ]
   ;
   tactic_atom:
-    [ [ n = integer -> TacGeneric (genarg_of_int n)
-      | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[]))
-      | "()" -> TacGeneric (genarg_of_unit ()) ] ]
+    [ [ n = integer -> { TacGeneric (genarg_of_int n) }
+      | r = reference -> { TacCall (Loc.tag ~loc (r,[])) }
+      | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
   ;
   match_key:
-    [ [ "match" -> Once
-      | "lazymatch" -> Select
-      | "multimatch" -> General ] ]
+    [ [ "match" -> { Once }
+      | "lazymatch" -> { Select }
+      | "multimatch" -> { General } ] ]
   ;
   input_fun:
-    [ [ "_" -> Name.Anonymous
-      | l = ident -> Name.Name l ] ]
+    [ [ "_" -> { Name.Anonymous }
+      | l = ident -> { Name.Name l } ] ]
   ;
   let_clause:
     [ [ idr = identref; ":="; te = tactic_expr ->
-         (CAst.map (fun id -> Name id) idr, arg_of_expr te)
-      | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr ->
-         (na, arg_of_expr te)
+         { (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
+      | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr ->
+         { (na, arg_of_expr te) }
       | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-         (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ]
+         { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ]
   ;
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        Subterm (oid, pc)
-      | pc = Constr.lconstr_pattern -> Term pc ] ]
+        { Subterm (oid, pc) }
+      | pc = Constr.lconstr_pattern -> { Term pc } ] ]
   ;
   match_hyps:
-    [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp)
-      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt)
+    [ [ na = name; ":"; mp =  match_pattern -> { Hyp (na, mp) }
+      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
       | na = name; ":="; mpv = match_pattern ->
-	  let t, ty =
+        { let t, ty =
 	    match mpv with
 	    | Term t -> (match t with
 	      | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty)
+	  in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) }
     ] ]
   ;
   match_context_rule:
     [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "=>"; te = tactic_expr -> Pat (largs, mp, te)
+        "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
       | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
-        "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
-      | "_"; "=>"; te = tactic_expr -> All te ] ]
+        "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
+      | "_"; "=>"; te = tactic_expr -> { All te } ] ]
   ;
   match_context_list:
-    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
+    [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
+      | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
   ;
   match_rule:
-    [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
-      | "_"; "=>"; te = tactic_expr -> All te ] ]
+    [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) }
+      | "_"; "=>"; te = tactic_expr -> { All te } ] ]
   ;
   match_list:
-    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
+    [ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
+      | "|"; mrl = LIST1 match_rule SEP "|" -> { mrl } ] ]
   ;
   message_token:
-    [ [ id = identref -> MsgIdent id
-      | s = STRING -> MsgString s
-      | n = integer -> MsgInt n ] ]
+    [ [ id = identref -> { MsgIdent id }
+      | s = STRING -> { MsgString s }
+      | n = integer -> { MsgInt n } ] ]
   ;
 
   ltac_def_kind:
-    [ [ ":=" -> false
-      | "::=" -> true ] ]
+    [ [ ":=" -> { false }
+      | "::=" -> { true } ] ]
   ;
 
   (* Definitions for tactics *)
   tacdef_body:
     [ [ name = Constr.global; it=LIST1 input_fun;
         redef = ltac_def_kind; body = tactic_expr ->
-          if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
+        { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
           else
             let id = reference_to_id name in
-            Tacexpr.TacticDefinition (id, TacFun (it, body))
+            Tacexpr.TacticDefinition (id, TacFun (it, body)) }
       | name = Constr.global; redef = ltac_def_kind;
         body = tactic_expr ->
-          if redef then Tacexpr.TacticRedefinition (name, body)
+        { if redef then Tacexpr.TacticRedefinition (name, body)
           else
             let id = reference_to_id name in
-            Tacexpr.TacticDefinition (id, body)
+            Tacexpr.TacticDefinition (id, body) }
     ] ]
   ;
   tactic:
-    [ [ tac = tactic_expr -> tac ] ]
+    [ [ tac = tactic_expr -> { tac } ] ]
   ;
 
   range_selector:
-    [ [ n = natural ; "-" ; m = natural -> (n, m)
-      | n = natural -> (n, n) ] ]
+    [ [ n = natural ; "-" ; m = natural -> { (n, m) }
+      | n = natural -> { (n, n) } ] ]
   ;
   (* We unfold a range selectors list once so that we can make a special case
    * for a unique SelectNth selector. *)
   range_selector_or_nth:
     [ [ n = natural ; "-" ; m = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
-          Goal_select.SelectList ((n, m) :: Option.default [] l)
+        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
+        { Goal_select.SelectList ((n, m) :: Option.default [] l) }
       | n = natural;
-        l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
-          let open Goal_select in
-          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
+        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
+        { let open Goal_select in
+          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
   ;
   selector_body:
-  [ [ l = range_selector_or_nth -> l
-    | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ]
+  [ [ l = range_selector_or_nth -> { l }
+    | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
   ;
   selector:
-    [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ]
+    [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ]
   ;
   toplevel_selector:
-    [ [ sel = selector_body; ":" -> sel
-    |   "!"; ":" -> Goal_select.SelectAlreadyFocused
-    |   IDENT "all"; ":" -> Goal_select.SelectAll ] ]
+    [ [ sel = selector_body; ":" -> { sel }
+    |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
+    |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
   ;
   tactic_mode:
-    [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g
-      | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ]
+    [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { tac g }
+      | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSubproof g } ] ]
   ;
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
-        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
-          Vernacexpr.VernacProof (Some (in_tac ta), l)
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
+          { Vernacexpr.VernacProof (Some (in_tac ta), l) } 
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
-          Vernacexpr.VernacProof (ta,Some l) ] ]
+        ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
+          { Vernacexpr.VernacProof (ta,Some l) } ] ]
   ;
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-          Hints.HintsExtern (n,c, in_tac tac) ] ]
+        { Hints.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
-          let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
-          CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
+        { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
+          CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ]
   ;
   END
 
+{
+
 open Stdarg
 open Tacarg
 open Vernacexpr
@@ -390,24 +398,36 @@ let vernac_solve n info tcom b =
 
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
-VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
-| [ toplevel_selector(s) ] -> [ s ]
+}
+
+VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector }
+| [ toplevel_selector(s) ] -> { s }
 END
 
+{
+
 let pr_ltac_info n = str "Info" ++ spc () ++ int n
 
-VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info
-| [ "Info" natural(n) ] -> [ n ]
+}
+
+VERNAC ARGUMENT EXTEND ltac_info PRINTED BY { pr_ltac_info }
+| [ "Info" natural(n) ] -> { n }
 END
 
+{
+
 let pr_ltac_use_default b =
   if b then (* Bug: a space is inserted before "..." *) str ".." else mt ()
 
-VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
-| [ "." ] -> [ false ]
-| [ "..." ] -> [ true ]
+}
+
+VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default }
+| [ "." ] -> { false }
+| [ "..." ] -> { true }
 END
 
+{
+
 let is_anonymous_abstract = function
   | TacAbstract (_,None) -> true
   | TacSolve [TacAbstract (_,None)] -> true
@@ -418,36 +438,44 @@ let rm_abstract = function
   | x -> x
 let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
-VERNAC tactic_mode EXTEND VernacSolve
-| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [ classify_as_proofstep ] -> [
+}
+
+VERNAC { tactic_mode } EXTEND VernacSolve
+| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
     vernac_solve g n t def
-  ]
-| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [
+  }
+| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    {
       let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
       let parallel = `Yes (solving_tac,anon_abstracting_tac) in
       let pbr = if solving_tac then Some "par" else None in
       VtProofStep{ parallel = parallel; proof_block_detection = pbr },
       VtLater
-    ] -> [
+    } -> {
       let t = rm_abstract t in
       vernac_solve Goal_select.SelectAll n t def
-    ]
+    }
 END
 
+{
+
 let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")"
 
-VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level
-| [ "(" "at" "level" natural(n) ")" ] -> [ n ]
+}
+
+VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY { pr_ltac_tactic_level }
+| [ "(" "at" "level" natural(n) ")" ] -> { n }
 END
 
 VERNAC ARGUMENT EXTEND ltac_production_sep
-| [ "," string(sep) ] -> [ sep ]
+| [ "," string(sep) ] -> { sep }
 END
 
+{
+
 let pr_ltac_production_item = function
 | Tacentries.TacTerm s -> quote (str s)
 | Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg
@@ -459,35 +487,38 @@ let pr_ltac_production_item = function
   in
   str arg ++ str "(" ++ Id.print id ++ sep ++ str ")"
 
-VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
-| [ string(s) ] -> [ Tacentries.TacTerm s ]
+}
+
+VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item }
+| [ string(s) ] -> { Tacentries.TacTerm s }
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ]
+  { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) }
 | [ ident(nt) ] ->
-  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ]
+  { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
+VERNAC COMMAND EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
-  [ VtSideff [], VtNow ] ->
-  [ fun ~atts ~st -> let open Vernacinterp in
+  { VtSideff [], VtNow } ->
+  { let open Vernacinterp in
       let n = Option.default 0 n in
       let deprecation = atts.deprecated in
       Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
-      st
-  ]
+  }
 END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  [ Feedback.msg_notice (Tacintern.print_ltac r) ]
+  { Feedback.msg_notice (Tacintern.print_ltac r) }
 END
 
 VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
 | [ "Locate" "Ltac" reference(r) ] ->
-  [ Tacentries.print_located_tactic r ]
+  { Tacentries.print_located_tactic r }
 END
 
+{
+
 let pr_ltac_ref = Libnames.pr_qualid
 
 let pr_tacdef_body tacdef_body =
@@ -506,23 +537,24 @@ let pr_tacdef_body tacdef_body =
   ++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
   ++ Pptactic.pr_raw_tactic body
 
+}
+
 VERNAC ARGUMENT EXTEND ltac_tacdef_body
-PRINTED BY pr_tacdef_body
-| [ tacdef_body(t) ] -> [ t ]
+PRINTED BY { pr_tacdef_body }
+| [ tacdef_body(t) ] -> { t }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
-| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
+VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
-  ] -> [ fun ~atts ~st -> let open Vernacinterp in
+  } -> { let open Vernacinterp in
            let deprecation = atts.deprecated in
            Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
-           st
-  ]
+  }
 END
 
 VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY
-| [ "Print" "Ltac" "Signatures" ] -> [ Tacentries.print_ltacs () ]
+| [ "Print" "Ltac" "Signatures" ] -> { Tacentries.print_ltacs () }
 END
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.mlg
index 1f56244c75..26f2b08d3a 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.mlg
@@ -12,6 +12,8 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
+{
+
 open Constrexpr
 open Constrexpr_ops
 open Stdarg
@@ -57,22 +59,26 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
 
 let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: withtac;
 
   withtac:
-    [ [ "with"; t = Tactic.tactic -> Some t
-      | -> None ] ]
+    [ [ "with"; t = Tactic.tactic -> { Some t }
+      | -> { None } ] ]
   ;
 
   Constr.closed_binder:
-    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
-          let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
-          [CLocalAssum ([id], default_binder_kind, typ)]
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> {
+          let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+          [CLocalAssum ([id], default_binder_kind, typ)] }
     ] ];
 
   END
 
+{
+
 open Obligations
 
 let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
@@ -80,77 +86,81 @@ let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl
 
 let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
 
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
+}
+
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
 | [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
-    [ obligation (num, Some name, Some t) tac ]
+    { obligation (num, Some name, Some t) tac }
 | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
-    [ obligation (num, Some name, None) tac ]
+    { obligation (num, Some name, None) tac }
 | [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
-    [ obligation (num, None, Some t) tac ]
+    { obligation (num, None, Some t) tac }
 | [ "Obligation" integer(num) withtac(tac) ] ->
-    [ obligation (num, None, None) tac ]
+    { obligation (num, None, None) tac }
 | [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
-    [ next_obligation (Some name) tac ]
-| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ]
+    { next_obligation (Some name) tac }
+| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
 | [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
-    [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
+    { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
-    [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
+    { try_solve_obligation num None (Some (Tacinterp.interp t)) }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF
 | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
-    [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
+    { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligations" "with" tactic(t) ] ->
-    [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
+    { try_solve_obligations None (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligations" ] ->
-    [ try_solve_obligations None None ]
+    { try_solve_obligations None None }
 END
 
 VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF
 | [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
-    [ solve_all_obligations (Some (Tacinterp.interp t)) ]
+    { solve_all_obligations (Some (Tacinterp.interp t)) }
 | [ "Solve" "All" "Obligations" ] ->
-    [ solve_all_obligations None ]
+    { solve_all_obligations None }
 END
 
 VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
-| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) }
+| [ "Admit" "Obligations" ] -> { admit_obligations None }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
-    fun ~atts ~st -> begin
+VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
         let open Vernacinterp in
         set_default_tactic
           (Locality.make_section_locality atts.locality)
           (Tacintern.glob_tactic t);
-        st
-      end]
+  }
 END
 
+{
+
 open Pp
 
+}
+
 VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
-| [ "Show" "Obligation" "Tactic" ] -> [
-    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
+| [ "Show" "Obligation" "Tactic" ] -> {
+    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
-| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ]
-| [ "Obligations" ] -> [ show_obligations None ]
+| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
+| [ "Obligations" ] -> { show_obligations None }
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ]
-| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ]
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
 END
 
-open Pp
+{
 
 (* Declare a printer for the content of Program tactics *)
 let () =
@@ -159,3 +169,5 @@ let () =
   | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
   in
   Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
+
+}
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.mlg
index f1634f1561..3e47724c4c 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.mlg
@@ -10,6 +10,8 @@
 
 (* Syntax for rewriting with strategies *)
 
+{
+
 open Names
 open Locus
 open Constrexpr
@@ -25,8 +27,14 @@ open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
 
+let wit_hyp = wit_var
+
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
+{
+
 type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
@@ -43,19 +51,23 @@ let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings
 let subst_glob_constr_with_bindings s c =
   Tacsubst.subst_glob_with_bindings s c
 
+}
+
 ARGUMENT EXTEND glob_constr_with_bindings
-    PRINTED BY pr_glob_constr_with_bindings_sign
+    PRINTED BY { pr_glob_constr_with_bindings_sign }
 
-    INTERPRETED BY interp_glob_constr_with_bindings
-    GLOBALIZED BY glob_glob_constr_with_bindings
-    SUBSTITUTED BY subst_glob_constr_with_bindings
+    INTERPRETED BY { interp_glob_constr_with_bindings }
+    GLOBALIZED BY { glob_glob_constr_with_bindings }
+    SUBSTITUTED BY { subst_glob_constr_with_bindings }
 
-    RAW_PRINTED BY pr_constr_expr_with_bindings
-    GLOB_PRINTED BY pr_glob_constr_with_bindings
+    RAW_PRINTED BY { pr_constr_expr_with_bindings }
+    GLOB_PRINTED BY { pr_glob_constr_with_bindings }
 
-   [ constr_with_bindings(bl) ] -> [ bl ]
+| [ constr_with_bindings(bl) ] -> { bl }
 END
 
+{
+
 type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
 type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
 
@@ -78,53 +90,61 @@ let pr_glob_strategy prc prlc _ (s : glob_strategy) =
   in
   Rewrite.pr_strategy prc prr s
 
+}
+
 ARGUMENT EXTEND rewstrategy
-    PRINTED BY pr_strategy
-
-    INTERPRETED BY interp_strategy
-    GLOBALIZED BY glob_strategy
-    SUBSTITUTED BY subst_strategy
-
-    RAW_PRINTED BY pr_raw_strategy
-    GLOB_PRINTED BY pr_glob_strategy
-
-    [ glob(c) ] -> [ StratConstr (c, true) ]
-  | [ "<-" constr(c) ] -> [ StratConstr (c, false) ]
-  | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ]
-  | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ]
-  | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ]
-  | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ]
-  | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ]
-  | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ]
-  | [ "id" ] -> [ StratId ]
-  | [ "fail" ] -> [ StratFail ]
-  | [ "refl" ] -> [ StratRefl ]
-  | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ]
-  | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ]
-  | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ]
-  | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ]
-  | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ]
-  | [ "(" rewstrategy(h) ")" ] -> [ h ]
-  | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ]
-  | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ]
-  | [ "hints" preident(h) ] -> [ StratHints (false, h) ]
-  | [ "terms" constr_list(h) ] -> [ StratTerms h ]
-  | [ "eval" red_expr(r) ] -> [ StratEval r ]
-  | [ "fold" constr(c) ] -> [ StratFold c ]
+    PRINTED BY { pr_strategy }
+
+    INTERPRETED BY { interp_strategy }
+    GLOBALIZED BY { glob_strategy }
+    SUBSTITUTED BY { subst_strategy }
+
+    RAW_PRINTED BY { pr_raw_strategy }
+    GLOB_PRINTED BY { pr_glob_strategy }
+
+  | [ glob(c) ] -> { StratConstr (c, true) }
+  | [ "<-" constr(c) ] -> { StratConstr (c, false) }
+  | [ "subterms" rewstrategy(h) ] -> { StratUnary (Subterms, h) }
+  | [ "subterm" rewstrategy(h) ] -> { StratUnary (Subterm, h) }
+  | [ "innermost" rewstrategy(h) ] -> { StratUnary(Innermost, h) }
+  | [ "outermost" rewstrategy(h) ] -> { StratUnary(Outermost, h) }
+  | [ "bottomup" rewstrategy(h) ] -> { StratUnary(Bottomup, h) }
+  | [ "topdown" rewstrategy(h) ] -> { StratUnary(Topdown, h) }
+  | [ "id" ] -> { StratId }
+  | [ "fail" ] -> { StratFail }
+  | [ "refl" ] -> { StratRefl }
+  | [ "progress" rewstrategy(h) ] -> { StratUnary (Progress, h) }
+  | [ "try" rewstrategy(h) ] -> { StratUnary (Try, h) }
+  | [ "any" rewstrategy(h) ] -> { StratUnary (Any, h) }
+  | [ "repeat" rewstrategy(h) ] -> { StratUnary (Repeat, h) }
+  | [ rewstrategy(h) ";" rewstrategy(h') ] -> { StratBinary (Compose, h, h') }
+  | [ "(" rewstrategy(h) ")" ] -> { h }
+  | [ "choice" rewstrategy(h) rewstrategy(h') ] -> { StratBinary (Choice, h, h') }
+  | [ "old_hints" preident(h) ] -> { StratHints (true, h) }
+  | [ "hints" preident(h) ] -> { StratHints (false, h) }
+  | [ "terms" constr_list(h) ] -> { StratTerms h }
+  | [ "eval" red_expr(r) ] -> { StratEval r }
+  | [ "fold" constr(c) ] -> { StratFold c }
 END
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
+{
+
 let db_strat db = StratUnary (Topdown, StratHints (false, db))
 let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
 
+}
+
 TACTIC EXTEND rewrite_strat
-| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
-| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
-| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
+| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
+| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) }
+| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None }
 END
 
+{
+
 let clsubstitute o c =
   Proofview.Goal.enter begin fun gl ->
   let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
@@ -137,59 +157,63 @@ let clsubstitute o c =
       (None :: List.map (fun id -> Some id) hyps)
   end
 
+}
+
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c }
 END
 
 
 (* Compatibility with old Setoids *)
 
 TACTIC EXTEND setoid_rewrite
-   [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-   -> [ cl_rewrite_clause c o AllOccurrences None ]
+ | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
+   -> { cl_rewrite_clause c o AllOccurrences None }
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-      [ cl_rewrite_clause c o AllOccurrences (Some id) ]
+      { cl_rewrite_clause c o AllOccurrences (Some id) }
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) None ]
+      { cl_rewrite_clause c o (occurrences_of occ) None }
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+      { cl_rewrite_clause c o (occurrences_of occ) (Some id) }
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+      { cl_rewrite_clause c o (occurrences_of occ) (Some id) }
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
+      { declare_relation a aeq n (Some lemma1) (Some lemma2) None }
 
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) None None ]
+      { declare_relation a aeq n (Some lemma1) None None }
   | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-      [ declare_relation a aeq n None None None ]
+      { declare_relation a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-    [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      [ declare_relation a aeq n None (Some lemma2) None ]
+      { declare_relation a aeq n None (Some lemma2) None }
   | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ]
+      { declare_relation a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ]
+      { declare_relation a aeq n (Some lemma1) None (Some lemma3) }
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
+      { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
   | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      [ declare_relation a aeq n None None (Some lemma3) ]
+      { declare_relation a aeq n None None (Some lemma3) }
 END
 
+{
+
 type binders_argtype = local_binder_expr list
 
 let wit_binders =
@@ -203,95 +227,92 @@ let () =
 
 open Pcoq
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: binders;
     binders:
-    [ [ b = Pcoq.Constr.binders -> b ] ];
+    [ [ b = Pcoq.Constr.binders -> { b } ] ];
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ]
+      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) None None ]
+      { declare_relation ~binders:b a aeq n (Some lemma1) None None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None None None ]
+      { declare_relation ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
+      { declare_relation ~binders:b a aeq n None (Some lemma2) None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
+      { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-    [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
+      { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ]
+      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
+      { declare_relation ~binders:b a aeq n None None (Some lemma3) }
 END
 
-VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ fun ~atts ~st -> let open Vernacinterp in
+VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
+  | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     { let open Vernacinterp in
          add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
-         st
-     ]
+     }
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ fun ~atts ~st -> let open Vernacinterp in
+     { let open Vernacinterp in
          add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
-         st
-     ]
+     }
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
-    => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
-    -> [ fun ~atts ~st -> let open Vernacinterp in
+    => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
+    -> { let open Vernacinterp in
            add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
-           st
-       ]
+       }
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ fun ~atts ~st -> let open Vernacinterp in
+    => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
+    -> { let open Vernacinterp in
            add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
-           st
-       ]
+       }
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ fun ~atts ~st -> let open Vernacinterp in
+    => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
+    -> { let open Vernacinterp in
            add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
-           st
-       ]
+       }
 END
 
 TACTIC EXTEND setoid_symmetry
-   [ "setoid_symmetry" ] -> [ setoid_symmetry ]
- | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ]
+ | [ "setoid_symmetry" ] -> { setoid_symmetry }
+ | [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n }
 END
 
 TACTIC EXTEND setoid_reflexivity
-[ "setoid_reflexivity" ] -> [ setoid_reflexivity ]
+| [ "setoid_reflexivity" ] -> { setoid_reflexivity }
 END
 
 TACTIC EXTEND setoid_transitivity
-  [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
-| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
+| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) }
+| [ "setoid_etransitivity" ] -> { setoid_transitivity None }
 END
 
 VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-  [ "Print" "Rewrite" "HintDb" preident(s) ] ->
-  [ let sigma, env = Pfedit.get_current_context () in
-    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ]
+| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+  { let sigma, env = Pfedit.get_current_context () in
+    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) }
 END
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.mlg
index 983e1578be..2713819c7b 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -8,13 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 (** Ltac profiling entrypoints *)
 
 open Profile_ltac
 open Stdarg
 
+}
+
 DECLARE PLUGIN "ltac_plugin"
 
+{
+
 let tclSET_PROFILING b =
    Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b))
 
@@ -33,42 +39,44 @@ let tclRESTART_TIMER s =
 let tclFINISH_TIMING ?(prefix="Timer") (s : string option) =
    Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s))
 
+}
+
 TACTIC EXTEND start_ltac_profiling
-| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ]
+| [ "start" "ltac" "profiling" ] -> { tclSET_PROFILING true }
 END
 
 TACTIC EXTEND stop_ltac_profiling
-| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ]
+| [ "stop" "ltac" "profiling" ] -> { tclSET_PROFILING false }
 END
 
 TACTIC EXTEND reset_ltac_profile
-| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ]
+| [ "reset" "ltac" "profile" ] -> { tclRESET_PROFILE }
 END
 
 TACTIC EXTEND show_ltac_profile
-| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ]
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ]
-| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ]
+| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
+| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
 END
 
 TACTIC EXTEND restart_timer
-| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ]
+| [ "restart_timer" string_opt(s) ] -> { tclRESTART_TIMER s }
 END
 
 TACTIC EXTEND finish_timing
-| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ]
-| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ]
+| [ "finish_timing" string_opt(s) ] -> { tclFINISH_TIMING ~prefix:"Timer" s }
+| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> { tclFINISH_TIMING ~prefix s }
 END
 
 VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
-  [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ]
+| [ "Reset" "Ltac" "Profile" ] -> { reset_profile () }
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ]
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
+| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
-  [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ]
+| [ "Show" "Ltac" "Profile" string(s) ] -> { print_results_tactic s }
 END