Removing the MetaIdArg entry of tactic expressions.

This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.

6 files changed, 1 insertions, 23 deletions

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/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/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/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