Remove a few tactics from the Tacexpr AST.

Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.

7 files changed, 59 insertions, 63 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index ce28eacc09..9879cfc280 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
 
+TACTIC EXTEND exact
+  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+END
+
 TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
@@ -197,6 +201,19 @@ TACTIC EXTEND intros_until
   [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ]
 END
 
+TACTIC EXTEND intro
+| [ "intro" ] -> [ Tactics.intro_move None MoveLast ]
+| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ]
+| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ]
+| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ]
+| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ]
+| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ]
+| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ]
+| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ]
+| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ]
+| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ]
+END
+
 (** Move *)
 
 TACTIC EXTEND move
@@ -206,6 +223,12 @@ TACTIC EXTEND move
 | [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
+(** Rename *)
+
+TACTIC EXTEND rename
+| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ]
+END
+
 (** Revert *)
 
 TACTIC EXTEND revert
@@ -222,6 +245,13 @@ TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
 
+(** Double induction *)
+
+TACTIC EXTEND double_induction
+  [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
+  [ Elim.h_double_induction h1 h2 ]
+END
+
 (* Admit *)
 
 TACTIC EXTEND admit
@@ -280,7 +310,6 @@ let initial_atomic () =
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl);
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
       ]
   in
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 0bddcc9fdd..e6d0a9c69c 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -15,6 +15,7 @@ open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Names
+open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
@@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob
   [ lconstr(c) ] -> [ c ]
 END
 
+let interp_casted_constr ist gl c =
+  interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
+
+ARGUMENT EXTEND casted_constr
+  TYPED AS constr
+  PRINTED BY pr_gen
+  INTERPRETED BY interp_casted_constr
+  [ constr(c) ] -> [ c ]
+END
+
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
 type loc_place = Id.t Loc.located gen_place
@@ -225,6 +236,14 @@ ARGUMENT EXTEND hloc
 
  END
 
+let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m
+
+ARGUMENT EXTEND rename
+  TYPED AS ident * ident
+  PRINTED BY pr_rename
+| [ ident(n) "into" ident(m) ] -> [ (n, m) ]
+END
+
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
 let pr_by_arg_tac _prc _prlc prtac opt_c =
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 4d1d8ba7fe..0cf77935c2 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
 
+val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
+
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
@@ -38,6 +40,11 @@ val wit_lconstr :
   Tacexpr.glob_constr_and_expr,
   Constr.t) Genarg.genarg_type
 
+val wit_casted_constr :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Constr.t) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 3744449e97..d39f835528 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -481,10 +481,6 @@ let rec intern_atomic lf ist x =
   (* Basic tactics *)
   | TacIntroPattern l ->
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
-  | TacIntroMove (ido,hto) ->
-      TacIntroMove (Option.map (intern_ident lf ist) ido,
-                    intern_move_location ist hto)
-  | TacExact c -> TacExact (intern_constr ist c)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
@@ -520,16 +516,6 @@ let rec intern_atomic lf ist x =
                Option.map (intern_or_and_intro_pattern_loc lf ist) ipats),
                Option.map (clause_app (intern_hyp_location ist)) cls)) l,
                Option.map (intern_constr_with_bindings ist) el))
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = intern_quantified_hypothesis ist h1 in
-      let h2 = intern_quantified_hypothesis ist h2 in
-      TacDoubleInduction (h1,h2)
-  (* Context management *)
-  | TacRename l ->
-      TacRename (List.map (fun (id1,id2) ->
-			     intern_hyp ist id1,
-			     intern_hyp ist id2) l)
-
   (* Conversion *)
   | TacReduce (r,cl) ->
       dump_glob_red_expr r;
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index fcc29a8302..5ee9b0fc4d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -684,10 +684,6 @@ let interp_typed_pattern ist env sigma (_,c,_) =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
   pattern_of_constr env sigma c
 
-(* Interprets a constr expression casted by the current goal *)
-let pf_interp_casted_constr ist gl c =
-  interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
-
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
@@ -1644,24 +1640,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
              expected behaviour. *)
           (Tactics.intro_patterns l')) sigma
       end }
-  | TacIntroMove (ido,hto) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let mloc = interp_move_location ist env sigma hto in
-        let ido = Option.map (interp_ident ist env sigma) ido in
-        name_atomic ~env
-          (TacIntroMove(ido,mloc))
-          (Tactics.intro_move ido mloc)
-      end }
-  | TacExact c ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
-        let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
-      end }
-      end
   | TacApply (a,ev,cb,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
@@ -1822,26 +1800,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = interp_quantified_hypothesis ist h1 in
-      let h2 = interp_quantified_hypothesis ist h2 in
-      name_atomic
-        (TacDoubleInduction (h1,h2))
-        (Elim.h_double_induction h1 h2)
-  (* Context management *)
-  | TacRename l ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
-        let l =
-          List.map (fun (id1,id2) ->
-	    interp_hyp ist env sigma id1,
-	    interp_ident ist env sigma (snd id2)) l
-        in
-        name_atomic ~env
-          (TacRename l)
-          (Tactics.rename_hyp l)
-      end }
 
   (* Conversion *)
   | TacReduce (r,cl) ->
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 8bb6ee4cdf..6f64981eff 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -72,6 +72,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
   Id.t Loc.located -> Id.t
 
+val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
+  Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
+
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
 
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 3f504b7f37..2c3c76ef74 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -137,8 +137,6 @@ let rec subst_match_goal_hyps subst = function
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l)
-  | TacIntroMove _ as x -> x
-  | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
@@ -162,10 +160,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
         subst_induction_arg subst c, ids, cls) l in
       let el' = Option.map (subst_glob_with_bindings subst) el in
       TacInductionDestruct (isrec,ev,(l',el'))
-  | TacDoubleInduction (h1,h2) as x -> x
-
-  (* Context management *)
-  | TacRename l as x -> x
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)