Removing "intro" from the tactic AST.

Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.

11 files changed, 29 insertions, 29 deletions

diff --git a/CHANGES b/CHANGES
index 9c89cdb8e..41d61ec45 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,9 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
+- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
+  a locally free identifier anymore. It must use e.g. the "fresh" primitive
+  instead (potential source of incompatibilities).
 
 Program
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4fe60538a..0a0927b3f 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -139,7 +139,6 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of 'dtrm intro_pattern_expr located list
-  | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 63b5463c4..efabdc4ad 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -197,6 +197,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
@@ -287,7 +300,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/tacintern.ml b/ltac/tacintern.ml
index 0f827755a..bd48ffb72 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -481,9 +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,
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index f6f988ee2..c8fa9367f 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1644,16 +1644,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
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 71dd718e8..1e974d6f5 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -137,7 +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)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9f19817dd..993695fb9 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,11 +528,6 @@ GEXTEND Gram
           TacAtom (!@loc, TacIntroPattern pl)
       | IDENT "intros" ->
           TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
-      | IDENT "intro"; id = ident; hto = move_location ->
-	  TacAtom (!@loc, TacIntroMove (Some id, hto))
-      | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
-      | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast))
-      | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast))
 
       | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
 
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 36511386a..5e43dfc42 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1074,16 +1074,19 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5192e2db1..e4d155499 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -816,7 +816,6 @@ module Make
       (* Printing tactics as arguments *)
       let rec pr_atom0 a = tag_atom a (match a with
         | TacIntroPattern [] -> primitive "intros"
-        | TacIntroMove (None,MoveLast) -> primitive "intro"
         | t -> str "(" ++ pr_atom1 t ++ str ")"
       )
 
@@ -828,13 +827,6 @@ module Make
         | TacIntroPattern (_::_ as p) ->
           hov 1 (primitive "intros" ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-        | TacIntroMove (None,MoveLast) as t ->
-          pr_atom0 t
-        | TacIntroMove (Some id,MoveLast) ->
-          primitive "intro" ++ spc () ++ pr_id id
-        | TacIntroMove (ido,hto) ->
-          hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
-                    Miscprint.pr_move_location pr.pr_name hto)
         | TacExact c ->
           hov 1 (primitive "exact" ++ pr_constrarg c)
         | TacApply (a,ev,cb,inhyp) ->
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index cc023cc3f..a3c265a21 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -417,6 +417,7 @@ Local Open Scope Int_scope.
     Let's do its job by hand: *)
 
 Ltac join_tac :=
+ let l := fresh "l" in
  intro l; induction l as [| lh ll _ lx lr Hlr];
    [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
      [ | destruct ((rh+2) <? lh) eqn:LT;
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index e57af7311..0c27d407c 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -109,6 +109,7 @@ Ltac intro_hyp_glob trm :=
     | Rabs => idtac
     | ?X1 =>
       let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable p) |- _ => idtac
           |  |- (derivable p) => idtac
@@ -250,6 +251,7 @@ Ltac intro_hyp_pt trm pt :=
       end
     | ?X1 =>
       let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable_pt p pt) |- _ => idtac
           |  |- (derivable_pt p pt) => idtac
@@ -341,8 +343,10 @@ Ltac is_diff_pt :=
     | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
       assumption
     | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     |  |- (True -> derivable_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_pt
     | _ =>
       try
@@ -411,6 +415,7 @@ Ltac is_diff_glob :=
       apply (derivable_comp X2 X1); is_diff_glob
     | _:(derivable ?X1) |- (derivable ?X1) => assumption
     |  |- (True -> derivable _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_glob
     | _ =>
       try
@@ -490,14 +495,17 @@ Ltac is_cont_pt :=
     | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       assumption
     | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       apply derivable_continuous_pt; assumption
     | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1);
         [ intro HypDDPT; apply HypDDPT
           | apply derivable_continuous; assumption ]
     |  |- (True -> continuity_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_pt
     | _ =>
       try
@@ -567,6 +575,7 @@ Ltac is_cont_glob :=
       apply (continuity_comp X2 X1); try is_cont_glob || assumption
     | _:(continuity ?X1) |- (continuity ?X1) => assumption
     |  |- (True -> continuity _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_glob
     | _:(derivable ?X1) |- (continuity ?X1) =>
       apply derivable_continuous; assumption