aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--intf/tacexpr.mli1
-rw-r--r--ltac/coretactics.ml414
-rw-r--r--ltac/tacintern.ml3
-rw-r--r--ltac/tacinterp.ml10
-rw-r--r--ltac/tacsubst.ml1
-rw-r--r--parsing/g_tactic.ml45
-rw-r--r--plugins/romega/ReflOmegaCore.v3
-rw-r--r--printing/pptactic.ml8
-rw-r--r--theories/MSets/MSetAVL.v1
-rw-r--r--theories/Reals/Ranalysis_reg.v9
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 08:38:43 +0000