Merge branch 'remove-quotations'

19 files changed, 42 insertions, 624 deletions

diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 6098de8f03..4432f4306e 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -60,7 +60,6 @@ G_ltac
 G_constr
 
 Q_util
-Q_coqast
 Egramml
 Argextend
 Tacextend
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
deleted file mode 100644
index f6abe12cf2..0000000000
--- a/grammar/q_coqast.ml4
+++ /dev/null
@@ -1,573 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Q_util
-open Compat
-
-let is_meta s = String.length s > 0 && s.[0] == '$'
-
-let purge_str s =
-  if String.length s == 0 || s.[0] <> '$' then s
-  else String.sub s 1 (String.length s - 1)
-
-let anti loc x =
-  expl_anti loc <:expr< $lid:purge_str x$ >>
-
-(* We don't give location for tactic quotation! *)
-let loc = CompatLoc.ghost
-
-let dloc = <:expr< Loc.ghost >>
-
-let mlexpr_of_ident id =
-  <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >>
-
-let mlexpr_of_name = function
-  | Names.Anonymous -> <:expr< Names.Anonymous >>
-  | Names.Name id ->
-      <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >>
-
-let mlexpr_of_dirpath dir =
-  let l = Names.DirPath.repr dir in
-  <:expr< Names.DirPath.make $mlexpr_of_list mlexpr_of_ident l$ >>
-
-let mlexpr_of_qualid qid =
-  let (dir, id) = Libnames.repr_qualid qid in
-  <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
-
-let mlexpr_of_reference = function
-  | Libnames.Qualid (loc,qid) ->
-    let loc = of_coqloc loc in <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
-  | Libnames.Ident (loc,id) ->
-    let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
-
-let mlexpr_of_union f g = function
-  | Util.Inl a -> <:expr< Util.Inl $f a$ >>
-  | Util.Inr b -> <:expr< Util.Inr $g b$ >>
-
-let mlexpr_of_located f (loc,x) =
-  let loc = of_coqloc loc in
-  <:expr< ($dloc$, $f x$) >>
-
-let mlexpr_of_loc loc = <:expr< $dloc$ >>
-
-let mlexpr_of_by_notation f = function
-  | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >>
-  | Misctypes.ByNotation (loc,s,sco) ->
-      let loc = of_coqloc loc in
-      <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
-
-let mlexpr_of_global_flag = function
-  | Tacexpr.TacGlobal -> <:expr<Tacexpr.TacGlobal>>
-  | Tacexpr.TacLocal  -> <:expr<Tacexpr.TacLocal>>
-
-let mlexpr_of_intro_pattern_disjunctive = function
-  _ -> failwith "mlexpr_of_intro_pattern_disjunctive: TODO"
-
-let mlexpr_of_intro_pattern_naming = function
-  | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
-  | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
-  | Misctypes.IntroIdentifier id ->
-      <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
-
-let mlexpr_of_intro_pattern = function
-  | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
-  | Misctypes.IntroNaming pat ->
-      <:expr< Misctypes.IntroNaming $mlexpr_of_intro_pattern_naming pat$ >>
-  | Misctypes.IntroAction _ ->
-      failwith "mlexpr_of_intro_pattern: TODO"
-
-let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
-
-let mlexpr_of_quantified_hypothesis = function
-  | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
-  | Misctypes.NamedHyp id ->  <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
-
-let mlexpr_of_or_var f = function
-  | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
-  | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
-
-let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident)
-
-let mlexpr_of_occs = function
-  | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
-  | Locus.AllOccurrencesBut l ->
-    <:expr< Locus.AllOccurrencesBut
-      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
-  | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >>
-  | Locus.OnlyOccurrences l ->
-    <:expr< Locus.OnlyOccurrences
-      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
-
-let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
-
-let mlexpr_of_hyp_location = function
-  | occs, Locus.InHyp ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >>
-  | occs, Locus.InHypTypeOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >>
-  | occs, Locus.InHypValueOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >>
-
-let mlexpr_of_clause cl =
-  <:expr< {Locus.onhyps=
-             $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
-               cl.Locus.onhyps$;
-           Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
-
-let mlexpr_of_red_flags {
-  Genredexpr.rBeta = bb;
-  Genredexpr.rIota = bi;
-  Genredexpr.rZeta = bz;
-  Genredexpr.rDelta = bd;
-  Genredexpr.rConst = l
-} = <:expr< {
-  Genredexpr.rBeta = $mlexpr_of_bool bb$;
-  Genredexpr.rIota = $mlexpr_of_bool bi$;
-  Genredexpr.rZeta = $mlexpr_of_bool bz$;
-  Genredexpr.rDelta = $mlexpr_of_bool bd$;
-  Genredexpr.rConst = $mlexpr_of_list (mlexpr_of_by_notation mlexpr_of_reference) l$
-} >>
-
-let mlexpr_of_instance c = <:expr< None >>
-
-let mlexpr_of_explicitation = function
-  | Constrexpr.ExplByName id -> <:expr< Constrexpr.ExplByName $mlexpr_of_ident id$ >>
-  | Constrexpr.ExplByPos (n,_id) -> <:expr< Constrexpr.ExplByPos $mlexpr_of_int n$ >>
-
-let mlexpr_of_binding_kind = function
-  | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >>
-  | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >>
-
-let mlexpr_of_binder_kind = function
-  | Constrexpr.Default b -> <:expr< Constrexpr.Default $mlexpr_of_binding_kind b$ >>
-  | Constrexpr.Generalized (b,b',b'') ->
-      <:expr< Constrexpr.TypeClass $mlexpr_of_binding_kind b$
-	$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
-
-let rec mlexpr_of_constr = function
-  | Constrexpr.CRef (Libnames.Ident (loc,id),_) when is_meta (Id.to_string id) ->
-      let loc = of_coqloc loc in
-      anti loc (Id.to_string id)
-  | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >>
-  | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CProdN (loc,l,a) ->
-      let loc = of_coqloc loc in
-      <:expr< Constrexpr.CProdN $dloc$ $mlexpr_of_list
-      (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Constrexpr.CLambdaN (loc,l,a) ->
-    let loc = of_coqloc loc in
-    <:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CAppExpl (loc,(p,r,us),l) ->
-    let loc = of_coqloc loc in
-    let a = (p,r,us) in
-    <:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_triple (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference mlexpr_of_instance a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Constrexpr.CApp (loc,a,l) ->
-    let loc = of_coqloc loc in
-    <:expr< Constrexpr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
-  | Constrexpr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Constrexpr.CHole (loc, None, ipat, None) ->
-    let loc = of_coqloc loc in
-    <:expr< Constrexpr.CHole $dloc$ None $mlexpr_of_intro_pattern_naming ipat$ None >>
-  | Constrexpr.CHole (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Constrexpr.CNotation(_,ntn,(subst,substl,[])) ->
-      <:expr< Constrexpr.CNotation $dloc$ $mlexpr_of_string ntn$
-              ($mlexpr_of_list mlexpr_of_constr subst$,
-               $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
-  | Constrexpr.CPatVar (loc,n) ->
-      let loc = of_coqloc loc in
-      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_ident n$ >>
-  | Constrexpr.CEvar (loc,n,[]) ->
-      let loc = of_coqloc loc in
-      <:expr< Constrexpr.CEvar $dloc$ $mlexpr_of_ident n$ [] >>
-  | _ -> failwith "mlexpr_of_constr: TODO"
-
-let mlexpr_of_occ_constr =
-  mlexpr_of_occurrences mlexpr_of_constr
-
-let mlexpr_of_occ_ref_or_constr =
-  mlexpr_of_occurrences
-    (mlexpr_of_union
-       (mlexpr_of_by_notation mlexpr_of_reference) mlexpr_of_constr)
-
-let mlexpr_of_red_expr = function
-  | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
-  | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
-  | Genredexpr.Simpl (f,o) ->
-      <:expr< Genredexpr.Simpl $mlexpr_of_red_flags f$ $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
-  | Genredexpr.Cbv f ->
-      <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
-  | Genredexpr.Cbn f ->
-      <:expr< Genredexpr.Cbn $mlexpr_of_red_flags f$ >>
-  | Genredexpr.Lazy f ->
-      <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >>
-  | Genredexpr.Unfold l ->
-      let f1 = mlexpr_of_by_notation mlexpr_of_reference in
-      let f = mlexpr_of_list (mlexpr_of_occurrences f1) in
-      <:expr< Genredexpr.Unfold $f l$ >>
-  | Genredexpr.Fold l ->
-      <:expr< Genredexpr.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Genredexpr.Pattern l ->
-      let f = mlexpr_of_list mlexpr_of_occ_constr in
-      <:expr< Genredexpr.Pattern $f l$ >>
-  | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
-  | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
-  | Genredexpr.ExtraRedExpr s ->
-      <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
-
-let rec mlexpr_of_argtype loc = function
-  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.PairArgType (t1,t2) ->
-      let t1 = mlexpr_of_argtype loc t1 in
-      let t2 = mlexpr_of_argtype loc t2 in
-      <:expr< Genarg.PairArgType $t1$ $t2$ >>
-  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-
-let mlexpr_of_may_eval f = function
-  | Genredexpr.ConstrEval (r,c) ->
-      <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >>
-  | Genredexpr.ConstrContext ((loc,id),c) ->
-      let loc = of_coqloc loc in
-      let id = mlexpr_of_ident id in
-      <:expr< Genredexpr.ConstrContext (loc,$id$) $f c$ >>
-  | Genredexpr.ConstrTypeOf c ->
-      <:expr< Genredexpr.ConstrTypeOf $mlexpr_of_constr c$ >>
-  | Genredexpr.ConstrTerm c ->
-      <:expr< Genredexpr.ConstrTerm $mlexpr_of_constr c$ >>
-
-let mlexpr_of_binding_kind = function
-  | Misctypes.ExplicitBindings l ->
-      let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
-      <:expr< Misctypes.ExplicitBindings $l$ >>
-  | Misctypes.ImplicitBindings l ->
-      let l = mlexpr_of_list mlexpr_of_constr l in
-      <:expr< Misctypes.ImplicitBindings $l$ >>
-  | Misctypes.NoBindings ->
-       <:expr< Misctypes.NoBindings >>
-
-let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr
-
-let mlexpr_of_constr_with_binding =
-  mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind
-
-let mlexpr_of_constr_with_binding_arg =
-  mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding
-
-let mlexpr_of_move_location f = function
-  | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >>
-  | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >>
-  | Misctypes.MoveFirst -> <:expr< Misctypes.MoveFirst >>
-  | Misctypes.MoveLast -> <:expr< Misctypes.MoveLast >>
-
-let mlexpr_of_induction_arg = function
-  | Tacexpr.ElimOnConstr c ->
-      <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >>
-  | Tacexpr.ElimOnIdent (_,id) ->
-      <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >>
-  | Tacexpr.ElimOnAnonHyp n ->
-      <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >>
-
-let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO"
-
-let mlexpr_of_pattern_ast = mlexpr_of_constr
-
-let mlexpr_of_entry_type = function
-    _ -> failwith "mlexpr_of_entry_type: TODO"
-
-let mlexpr_of_match_lazy_flag = function
-  | Tacexpr.General -> <:expr<Tacexpr.General>>
-  | Tacexpr.Select    -> <:expr<Tacexpr.Select>>
-  | Tacexpr.Once    -> <:expr<Tacexpr.Once>>
-
-let mlexpr_of_match_pattern = function
-  | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >>
-  | Tacexpr.Subterm (b,ido,t) ->
-      <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
-
-let mlexpr_of_match_context_hyps = function
-  | Tacexpr.Hyp (id,l) ->
-      let f = mlexpr_of_located mlexpr_of_name in
-      <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >>
-  | Tacexpr.Def (id,v,l) ->
-      let f = mlexpr_of_located mlexpr_of_name in
-      <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >>
-
-let mlexpr_of_match_rule f = function
-  | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >>
-  | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >>
-
-let mlexpr_of_message_token = function
-  | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >>
-  | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
-  | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
-
-let mlexpr_of_debug = function
-  | Tacexpr.Off -> <:expr< Tacexpr.Off >>
-  | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
-  | Tacexpr.Info -> <:expr< Tacexpr.Info >>
-
-let rec mlexpr_of_atomic_tactic = function
-  (* Basic tactics *)
-  | Tacexpr.TacIntroPattern pl ->
-      let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
-      <:expr< Tacexpr.TacIntroPattern $pl$ >>
-  | Tacexpr.TacIntroMove (idopt,idopt') ->
-      let idopt = mlexpr_of_ident_option idopt in
-      let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
-      <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >>
-  | Tacexpr.TacExact c ->
-      <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
-  | Tacexpr.TacApply (b,false,cb,None) ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding_arg cb$ None >>
-  | Tacexpr.TacElim (false,cb,cbo) ->
-      let cb = mlexpr_of_constr_with_binding_arg cb in
-      let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
-      <:expr< Tacexpr.TacElim False $cb$ $cbo$ >>
-  | Tacexpr.TacCase (false,cb) ->
-      let cb = mlexpr_of_constr_with_binding_arg cb in
-      <:expr< Tacexpr.TacCase False $cb$ >>
-  | Tacexpr.TacFix (ido,n) ->
-      let ido = mlexpr_of_ident_option ido in
-      let n = mlexpr_of_int n in
-      <:expr< Tacexpr.TacFix $ido$ $n$ >>
-  | Tacexpr.TacMutualFix (id,n,l) ->
-      let id = mlexpr_of_ident id in
-      let n = mlexpr_of_int n in
-      let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
-      let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >>
-  | Tacexpr.TacCofix ido ->
-      let ido = mlexpr_of_ident_option ido in
-      <:expr< Tacexpr.TacCofix $ido$ >>
-  | Tacexpr.TacMutualCofix (id,l) ->
-      let id = mlexpr_of_ident id in
-      let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
-      let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
-
-  | Tacexpr.TacAssert (b,t,ipat,c) ->
-      let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in
-      <:expr< Tacexpr.TacAssert $mlexpr_of_bool b$
-              $mlexpr_of_option mlexpr_of_tactic t$ $ipat$
-	      $mlexpr_of_constr c$ >>
-  | Tacexpr.TacGeneralize cl ->
-      <:expr< Tacexpr.TacGeneralize
-	      $mlexpr_of_list
-                (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >>
-  | Tacexpr.TacGeneralizeDep c ->
-      <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
-  | Tacexpr.TacLetTac (na,c,cl,b,e) ->
-      let na = mlexpr_of_name na in
-      let cl = mlexpr_of_clause_pattern cl in
-      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$
-	      $mlexpr_of_bool b$
-	      (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e)
-      >>
-
-  (* Derived basic tactics *)
-  | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
-      <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
-	$mlexpr_of_pair
-	(mlexpr_of_list
-	   (mlexpr_of_triple
-	      (mlexpr_of_pair
-                 (mlexpr_of_option mlexpr_of_bool)
-                 mlexpr_of_induction_arg)
-	      (mlexpr_of_pair
-		 (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern_naming))
-		 (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive)))
-	      (mlexpr_of_option mlexpr_of_clause)))
-	(mlexpr_of_option mlexpr_of_constr_with_binding)
- l$ >>
-
-  (* Context management *)
-  | Tacexpr.TacClear (b,l) ->
-      let l = mlexpr_of_list (mlexpr_of_hyp) l in
-      <:expr< Tacexpr.TacClear $mlexpr_of_bool b$ $l$ >>
-  | Tacexpr.TacClearBody l ->
-      let l = mlexpr_of_list (mlexpr_of_hyp) l in
-      <:expr< Tacexpr.TacClearBody $l$ >>
-  | Tacexpr.TacMove (id1,id2) ->
-      <:expr< Tacexpr.TacMove
-              $mlexpr_of_hyp id1$
-              $mlexpr_of_move_location mlexpr_of_hyp id2$ >>
-
-  (* Constructors *)
-  | Tacexpr.TacSplit (ev,l) ->
-      <:expr< Tacexpr.TacSplit
-        ($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>>
-  (* Conversion *)
-  | Tacexpr.TacReduce (r,cl) ->
-      let l = mlexpr_of_clause cl in
-      <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
-  | Tacexpr.TacChange (p,c,cl) ->
-      let l = mlexpr_of_clause cl in
-      let g = mlexpr_of_option mlexpr_of_constr in
-      <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >>
-
-  (* Equivalence relations *)
-  | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
-
-  | _ -> failwith "Quotation of atomic tactic expressions: TODO"
-
-and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
-  | Tacexpr.TacAtom (loc,t) ->
-      let loc = of_coqloc loc in
-      <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >>
-  | Tacexpr.TacThen (t1,t2) ->
-      <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$>>
-  | Tacexpr.TacThens (t,tl) ->
-      <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>>
-  | Tacexpr.TacFirst tl ->
-      <:expr< Tacexpr.TacFirst $mlexpr_of_list mlexpr_of_tactic tl$ >>
-  | Tacexpr.TacSolve tl ->
-      <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >>
-  | Tacexpr.TacTry t ->
-      <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacOr (t1,t2) ->
-      <:expr< Tacexpr.TacOr $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
-  | Tacexpr.TacOrelse (t1,t2) ->
-      <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >>
-  | Tacexpr.TacDo (n,t) ->
-      <:expr< Tacexpr.TacDo $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacTimeout (n,t) ->
-      <:expr< Tacexpr.TacTimeout $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacRepeat t ->
-      <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacProgress t ->
-      <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacShowHyps t ->
-      <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacId l ->
-      <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
-  | Tacexpr.TacFail (g,n,l) ->
-      <:expr< Tacexpr.TacFail $mlexpr_of_global_flag g$ $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >>
-(*
-  | Tacexpr.TacInfo t -> TacInfo (loc,f t)
-
-  | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t)))
-  | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t)
-*)
-  | Tacexpr.TacLetIn (isrec,l,t) ->
-      let f =
-	mlexpr_of_pair
-	  (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident)
-	  mlexpr_of_tactic_arg in
-      <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacMatch (lz,t,l) ->
-      <:expr< Tacexpr.TacMatch
-        $mlexpr_of_match_lazy_flag lz$
-        $mlexpr_of_tactic t$
-        $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-  | Tacexpr.TacMatchGoal (lz,lr,l) ->
-      <:expr< Tacexpr.TacMatchGoal
-        $mlexpr_of_match_lazy_flag lz$
-        $mlexpr_of_bool lr$
-        $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-
-  | Tacexpr.TacFun (idol,body) ->
-      <:expr< Tacexpr.TacFun
-        ($mlexpr_of_list mlexpr_of_ident_option idol$,
-         $mlexpr_of_tactic body$) >>
-  | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
-  | Tacexpr.TacArg (_,t) ->
-      <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >>
-  | Tacexpr.TacComplete t ->
-      <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >>
-  | _ -> failwith "Quotation of tactic expressions: TODO"
-
-and mlexpr_of_tactic_arg = function
-  | Tacexpr.MetaIdArg (loc,true,id) ->
-    let loc = of_coqloc loc in
-    anti loc id
-  | Tacexpr.MetaIdArg (loc,false,id) ->
-    let loc = of_coqloc loc in
-    <:expr< Tacexpr.ConstrMayEval (Genredexpr.ConstrTerm $anti loc id$) >>
-  | Tacexpr.TacCall (loc,t,tl) ->
-    let loc = of_coqloc loc in
-    <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>>
-  | Tacexpr.Tacexp t ->
-      <:expr< Tacexpr.Tacexp $mlexpr_of_tactic t$ >>
-  | Tacexpr.ConstrMayEval c ->
-      <:expr< Tacexpr.ConstrMayEval $mlexpr_of_may_eval mlexpr_of_constr c$ >>
-  | Tacexpr.Reference r ->
-      <:expr< Tacexpr.Reference $mlexpr_of_reference r$ >>
-  | _ -> failwith "mlexpr_of_tactic_arg: TODO"
-
-
-IFDEF CAMLP5 THEN
-
-let not_impl x =
-  let desc =
-    if Obj.is_block (Obj.repr x) then
-      "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
-    else "int_val = " ^ string_of_int (Obj.magic x)
-  in
-  failwith ("<Q_coqast.patt_of_expt, not impl: " ^ desc)
-
-(* The following function is written without quotation
-   in order to be parsable even by camlp4. The version with
-   quotation can be found in revision <= 12972 of [q_util.ml4] *)
-
-open MLast
-
-let rec patt_of_expr e =
-  let loc = loc_of_expr e in
-  match e with
-    | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2)
-    | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2)
-    | ExLid (_, x) when x = vala "loc" -> PaAny loc
-    | ExLid (_, s) -> PaLid (loc, s)
-    | ExUid (_, s) -> PaUid (loc, s)
-    | ExStr (_, s) -> PaStr (loc, s)
-    | ExAnt (_, e) -> PaAnt (loc, patt_of_expr e)
-    | _ -> not_impl e
-
-let fconstr e =
-  let ee s =
-    mlexpr_of_constr (Pcoq.Gram.entry_parse e
-			(Pcoq.Gram.parsable (Stream.of_string s)))
-  in
-  let ep s = patt_of_expr (ee s) in
-  Quotation.ExAst (ee, ep)
-
-let ftac e =
-  let ee s =
-    mlexpr_of_tactic (Pcoq.Gram.entry_parse e
-			(Pcoq.Gram.parsable (Stream.of_string s)))
-  in
-  let ep s = patt_of_expr (ee s) in
-  Quotation.ExAst (ee, ep)
-
-let _ =
-  Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi);
-  Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi);
-  Quotation.default := "constr"
-
-ELSE
-
-open Pcaml
-
-let expand_constr_quot_expr loc _loc_name_opt contents =
-  mlexpr_of_constr
-    (Pcoq.Gram.parse_string Pcoq.Constr.constr_eoi loc contents)
-
-let expand_tactic_quot_expr loc _loc_name_opt contents =
-  mlexpr_of_tactic
-    (Pcoq.Gram.parse_string Pcoq.Tactic.tactic_eoi loc contents)
-
-let _ =
-  (* FIXME: for the moment, we add quotations in expressions only, not pattern *)
-  Quotation.add "constr" Quotation.DynAst.expr_tag expand_constr_quot_expr;
-  Quotation.add "tactic" Quotation.DynAst.expr_tag expand_tactic_quot_expr;
-  Quotation.default := "constr"
-
-END
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 4b0be1b1cb..c6e2e99668 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -54,9 +54,11 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
+let mlexpr_of_ident id =
+  <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >>
+
 let mlexpr_of_token = function
 | Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >>
-| Tok.METAIDENT s -> <:expr< Tok.METAIDENT $mlexpr_of_string s$ >>
 | Tok.PATTERNIDENT s -> <:expr< Tok.PATTERNIDENT $mlexpr_of_string s$ >>
 | Tok.IDENT s -> <:expr< Tok.IDENT $mlexpr_of_string s$ >>
 | Tok.FIELD s -> <:expr< Tok.FIELD $mlexpr_of_string s$ >>
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 50827ead25..d0e0dab22e 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -34,6 +34,8 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
+val mlexpr_of_ident : Names.Id.t -> MLast.expr
+
 val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
 
 val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index ef7cdbfa3a..10afcdd21a 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -15,7 +15,6 @@ open Pp
 open Names
 open Genarg
 open Q_util
-open Q_coqast
 open Argextend
 open Pcoq
 open Egramml
@@ -32,6 +31,15 @@ let rec make_patt = function
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
+let rec mlexpr_of_argtype loc = function
+  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
+  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
+  | Genarg.PairArgType (t1,t2) ->
+      let t1 = mlexpr_of_argtype loc t1 in
+      let t2 = mlexpr_of_argtype loc t2 in
+      <:expr< Genarg.PairArgType $t1$ $t2$ >>
+  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
+
 let rec make_when loc = function
   | [] -> <:expr< True >>
   | ExtNonTerminal (t, _, p) :: l ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 57c61874a5..502f2db4c1 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -206,7 +206,6 @@ constraint 'a = <
 
 and 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
-  | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
   | UConstr        of 'utrm
   | Reference      of 'ref
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 3405d2429b..0e416fe32c 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -262,7 +262,6 @@ IFDEF CAMLP5 THEN
     let pattern = match tok with
     | Tok.KEYWORD s -> "", s
     | Tok.IDENT s -> "IDENT", s
-    | Tok.METAIDENT s -> "METAIDENT", s
     | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
     | Tok.FIELD s -> "FIELD", s
     | Tok.INT s -> "INT", s
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1ac260ebeb..0fe0ac42b1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -132,10 +132,7 @@ GEXTEND Gram
   closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
-    [ [ id = Prim.ident -> id
-
-      (* This is used in quotations and Syntax *)
-      | id = METAIDENT -> Id.of_string id ] ]
+    [ [ id = Prim.ident -> id ] ]
   ;
   Prim.name:
     [ [ "_" -> (!@loc, Anonymous) ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 12d53030d7..0a11d3928a 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -146,7 +146,6 @@ GEXTEND Gram
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
       (* Unambigous entries: tolerated w/o "ltac:" modifier *)
-      | id = METAIDENT -> MetaIdArg (!@loc,true,id)
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
@@ -179,8 +178,7 @@ GEXTEND Gram
       | c = Constr.constr -> ConstrTerm c ] ]
   ;
   tactic_atom:
-    [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id)
-      | n = integer -> TacGeneric (genarg_of_int n)
+    [ [ n = integer -> TacGeneric (genarg_of_int n)
       | r = reference -> TacCall (!@loc,r,[])
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 74e05ce84d..232e9aee3f 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -493,7 +493,6 @@ let process_chars bp c cs =
         err (bp, ep') Undefined_token
 
 let token_of_special c s = match c with
-  | '$' -> METAIDENT s
   | '.' -> FIELD s
   | _ -> assert false
 
@@ -532,8 +531,6 @@ let blank_or_eof cs =
 let rec next_token = parser bp
   | [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
       comm_loc bp; push_char c; next_token s
-  | [< ''$' as c; t = parse_after_special c bp >] ep ->
-      comment_stop bp; (t, (ep, bp))
   | [< ''.' as c; t = parse_after_special c bp; s >] ep ->
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 4f50c48d0d..6b90086155 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -10,7 +10,6 @@
 
 type t =
   | KEYWORD of string
-  | METAIDENT of string
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
@@ -24,7 +23,6 @@ type t =
 let equal t1 t2 = match t1, t2 with
 | IDENT s1, KEYWORD s2 -> CString.equal s1 s2
 | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
-| METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
 | PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
 | IDENT s1, IDENT s2 -> CString.equal s1 s2
 | FIELD s1, FIELD s2 -> CString.equal s1 s2
@@ -40,7 +38,6 @@ let extract_string = function
   | KEYWORD s -> s
   | IDENT s -> s
   | STRING s -> s
-  | METAIDENT s -> s
   | PATTERNIDENT s -> s
   | FIELD s -> s
   | INT s -> s
@@ -52,7 +49,6 @@ let extract_string = function
 let to_string = function
   | KEYWORD s -> Format.sprintf "%S" s
   | IDENT s -> Format.sprintf "IDENT %S" s
-  | METAIDENT s -> Format.sprintf "METAIDENT %S" s
   | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
   | FIELD s -> Format.sprintf "FIELD %S" s
   | INT s -> Format.sprintf "INT %s" s
@@ -76,7 +72,6 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok)
 let of_pattern = function
   | "", s -> KEYWORD s
   | "IDENT", s -> IDENT s
-  | "METAIDENT", s -> METAIDENT s
   | "PATTERNIDENT", s -> PATTERNIDENT s
   | "FIELD", s -> FIELD s
   | "INT", s -> INT s
@@ -90,7 +85,6 @@ let of_pattern = function
 let to_pattern = function
   | KEYWORD s -> "", s
   | IDENT s -> "IDENT", s
-  | METAIDENT s -> "METAIDENT", s
   | PATTERNIDENT s -> "PATTERNIDENT", s
   | FIELD s -> "FIELD", s
   | INT s -> "INT", s
@@ -105,7 +99,6 @@ let match_pattern =
   function
     | "", "" -> (function KEYWORD s -> s | _ -> err ())
     | "IDENT", "" -> (function IDENT s -> s | _ -> err ())
-    | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ())
     | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
     | "FIELD", "" -> (function FIELD s -> s | _ -> err ())
     | "INT", "" -> (function INT s -> s | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index f37de05a44..416ce468e3 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -10,7 +10,6 @@
 
 type t =
   | KEYWORD of string
-  | METAIDENT of string
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index c96b4a4f4a..04c62eb487 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -17,15 +17,22 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+open Names
 open Coq_omega
 
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
+
 let omega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No Omega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b36..6b2b2bbfaf 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,15 +10,22 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
 
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
+
 let romega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ed85b21478..12667d0f24 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1189,10 +1189,6 @@ module Make
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str "$" ++ str s)
-          | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 151949c3c6..85b9d6a08f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -752,11 +752,14 @@ let case_eq_intros_rewrite x =
   end }
 
 let rec find_a_destructable_match t =
+  let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
+  let cl = [cl, (None, None), None], None in
+  let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in
   match kind_of_term t with
     | Case (_,_,x,_) when closed0 x ->
 	if isVar x then
 	  (* TODO check there is no rel n. *)
-	  raise (Found (Tacinterp.eval_tactic(<:tactic<destruct x>>)))
+	  raise (Found (Tacinterp.eval_tactic dest))
 	else
 	  (* let _ = Pp.msgnl (Printer.pr_lconstr x)  in *)
 	  raise (Found (case_eq_intros_rewrite x))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4ef1beb034..cbb9db65c1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -35,11 +35,6 @@ let dloc = Loc.ghost
 let error_global_not_found_loc (loc,qid) =
   error_global_not_found_loc loc qid
 
-let error_syntactic_metavariables_not_allowed loc =
-  user_err_loc
-    (loc,"out_ident",
-     str "Syntactic metavariables allowed only in quotations.")
-
 let error_tactic_expected loc =
   user_err_loc (loc,"",str "Tactic expected.")
 
@@ -672,7 +667,6 @@ and intern_tactic_as_arg loc onlytac ist a =
   | Tacexp a -> a
   | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
-  | MetaIdArg _ -> assert false
 
 and intern_tactic_or_tacarg ist = intern_tactic false ist
 
@@ -686,13 +680,6 @@ and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | UConstr c -> UConstr (intern_constr ist c)
-  | MetaIdArg (loc,istac,s) ->
-      (* $id can occur in Grammar tactic... *)
-      let id = Id.of_string s in
-      if find_var id ist then
-	if istac then Reference (ArgVar (adjust_loc loc,id))
-	else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None))
-      else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
   | TacCall (loc,f,l) ->
       TacCall (loc,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cb4a9f320d..43c9ee9be4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1371,7 +1371,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
         let env = Proofview.Goal.env gl in
         Ftactic.return (Value.of_uconstr (interp_uconstr ist env c))
       end }
-  | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) ->
       interp_ltac_reference loc true ist r
   | TacCall (loc,f,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index dd851b5c0d..4a5fa9828e 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -260,7 +260,6 @@ and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
   | UConstr c -> UConstr (subst_glob_constr subst c)
-  | MetaIdArg (_loc,_,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
   | TacFreshId _ as x -> x