Moving the "specialize" tactic out of the AST. Also removed an obsolete

variant of it, accepting an additional integer.

9 files changed, 16 insertions, 31 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 01e01ff858..eeba560d71 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -128,7 +128,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       rec_flag * evars_flag * ('trm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecompose of 'ind list * 'trm
-  | TacSpecialize of int option * 'trm with_bindings
 
   (* Automation tactics *)
   | TacTrivial of debug * 'trm list * string list option
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3142522023..52973fef2c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -591,9 +591,6 @@ GEXTEND Gram
           TacGeneralize (((nl,c),na)::l)
       | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
 
-      | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
-	  TacSpecialize (n,lcb)
-
       (* Derived basic tactics *)
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
           TacSimpleInductionDestruct (true,h)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c7aff50866..6c2c67c352 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -722,10 +722,6 @@ and pr_atom1 = function
       hov 1 (str "decompose" ++ spc () ++
         hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
 	  ++ str "]" ++ pr_constrarg c))
-  | TacSpecialize (n,c) ->
-      hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
-             pr_with_bindings c)
-
   (* Automation tactics *)
   | TacTrivial (_,[],Some []) as x -> pr_atom0 x
   | TacTrivial (d,lems,db) ->
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index bff5c13d3f..63daab2275 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -103,3 +103,13 @@ TACTIC EXTEND eright_with
     Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true) sigma bl
   ]
 END
+
+(** Specialize *)
+
+TACTIC EXTEND specialize
+  [ "specialize" constr_with_bindings(c) ] -> [
+    let { Evd.sigma = sigma; it = c } = c in
+    let specialize c = Proofview.V82.tactic (Tactics.specialize c) in
+    Tacticals.New.tclWITHHOLES false specialize sigma c
+  ]
+END
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 7062737382..4d711af9ab 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -508,8 +508,6 @@ let rec intern_atomic lf ist x =
       TacDoubleInduction (h1,h2)
   | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
       TacDecompose (l,intern_constr ist c)
-  | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
-
   (* Context management *)
   | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
   | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ec8cb59ea5..1b770d214e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1633,16 +1633,6 @@ and interp_atomic ist tac =
         let l = List.map (interp_inductive ist) l in
         Elim.h_decompose l c
       end
-  | TacSpecialize (n,cb) ->
-      Proofview.Goal.raw_enter begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
-        Proofview.V82.tactic begin fun gl -> 
-          let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-          tclWITHHOLES false (Tactics.specialize n) sigma cb gl
-        end
-      end
-
   (* Context management *)
   | TacClear (b,l) ->
       Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 1ed6b6c27c..6222455240 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -169,7 +169,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacDecompose (l,c) ->
       let l = List.map (subst_or_var (subst_ind subst)) l in
       TacDecompose (l,subst_glob_constr subst c)
-  | TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
 
   (* Context management *)
   | TacClear _ as x -> x
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 00a35e2369..8ed8f18566 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1276,7 +1276,7 @@ let rec intros_clearing = function
 
 (* Modifying/Adding an hypothesis  *)
 
-let specialize mopt (c,lbind) g =
+let specialize (c,lbind) g =
   let tac, term =
     if lbind == NoBindings then
       let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
@@ -1287,15 +1287,11 @@ let specialize mopt (c,lbind) g =
       let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
       let nargs = List.length tstack in
-      let tstack = match mopt with
-	| Some m ->
-	    if m < nargs then List.firstn m tstack else tstack
-	| None ->
-	    let rec chk = function
-	      | [] -> []
-	      | t::l -> if occur_meta t then [] else t :: chk l
-	    in chk tstack
+      let rec chk = function
+      | [] -> []
+      | t::l -> if occur_meta t then [] else t :: chk l
       in
+      let tstack = chk tstack in
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta term then
 	errorlabstrm "" (str "Cannot infer an instance for " ++
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 81f63fc22b..411cc38f43 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -160,7 +160,7 @@ val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> tactic
 val keep          : Id.t list -> tactic
 
-val specialize    : int option -> constr with_bindings -> tactic
+val specialize    : constr with_bindings -> tactic
 
 val move_hyp      : bool -> Id.t -> Id.t move_location -> tactic
 val rename_hyp    : (Id.t * Id.t) list -> tactic