Merge branch 'remove-quotations'

4 files changed, 4 insertions, 16 deletions

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