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.

3 files changed, 0 insertions, 15 deletions

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