aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/tactics.rst30
-rw-r--r--plugins/ltac/g_tactic.mlg4
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml8
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tacsubst.ml3
-rw-r--r--tactics/tactics.ml11
-rw-r--r--tactics/tactics.mli2
-rw-r--r--test-suite/success/apply.v29
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
12 files changed, 68 insertions, 38 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 26a56005c1..4f01559cad 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -878,38 +878,38 @@ Applying theorems
This happens if the conclusion of :token:`ident` does not match any of
the non-dependent premises of the type of :token:`term`.
- .. tacv:: apply {+, @term} in @ident
+ .. tacv:: apply {+, @term} in {+, @ident}
- This applies each :token:`term` in sequence in :token:`ident`.
+ This applies each :token:`term` in sequence in each hypothesis :token:`ident`.
- .. tacv:: apply {+, @term with @bindings} in @ident
+ .. tacv:: apply {+, @term with @bindings} in {+, @ident}
- This does the same but uses the bindings in each :n:`(@ident := @term)` to
- instantiate the parameters of the corresponding type of :token:`term`
- (see :ref:`bindings`).
+ This does the same but uses the bindings to instantiate
+ parameters of :token:`term` (see :ref:`bindings`).
- .. tacv:: eapply {+, @term {? with @bindings } } in @ident
+ .. tacv:: eapply {+, @term {? with @bindings } } in {+, @ident}
This works as :tacn:`apply … in` but turns unresolved bindings into
existential variables, if any, instead of failing.
- .. tacv:: apply {+, @term {? with @bindings } } in @ident as @simple_intropattern
+ .. tacv:: apply {+, @term {? with @bindings } } in {+, @ident {? as @simple_intropattern}}
:name: apply … in … as
- This works as :tacn:`apply … in` then applies the :token:`simple_intropattern`
- to the hypothesis :token:`ident`.
+ This works as :tacn:`apply … in` but applying an associated
+ :token:`simple_intropattern` to each hypothesis :token:`ident`
+ that comes with such clause.
- .. tacv:: simple apply @term in @ident
+ .. tacv:: simple apply @term in {+, @ident}
This behaves like :tacn:`apply … in` but it reasons modulo conversion
only on subterms that contain no variables to instantiate and does not
traverse tuples. See :ref:`the corresponding example <simple_apply_ex>`.
- .. tacv:: {? simple} apply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
- {? simple} eapply {+, @term {? with @bindings}} in @ident {? as @simple_intropattern}
+ .. tacv:: {? simple} apply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
+ {? simple} eapply {+, @term {? with @bindings}} in {+, @ident {? as @simple_intropattern}}
- This summarizes the different syntactic variants of :n:`apply @term in @ident`
- and :n:`eapply @term in @ident`.
+ This summarizes the different syntactic variants of :n:`apply @term in {+, @ident}`
+ and :n:`eapply @term in {+, @ident}`.
.. tacn:: constructor @natural
:name: constructor
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 236de65462..465afcdfdb 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -407,8 +407,8 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
in_hyp_as:
- [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
- | -> { None } ] ]
+ [ [ "in"; l = LIST1 [id = id_or_meta; ipat = as_ipat -> { (id,ipat) } ] SEP "," -> { l }
+ | -> { [] } ] ]
;
orient_rw:
[ [ "->" -> { true }
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index edd56ee0f7..cd7b1f7f28 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -458,8 +458,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
let pr_in_hyp_as prc pr_id = function
- | None -> mt ()
- | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+ | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
let pr_in_clause pr_id = function
| { onhyps=None; concl_occs=NoOccurrences } ->
@@ -756,7 +755,7 @@ let pr_goal_selector ~toplevel s =
(if a then mt() else primitive "simple ") ++
primitive (with_evars ev "apply") ++ spc () ++
prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+ prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
)
| TacElim (ev,cb,cbo) ->
hov 1 (
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index eaedf8d9c1..7b2c8e1d04 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -108,7 +108,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 50767821e4..2382dcfbb9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -107,7 +107,7 @@ type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
| TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
- ('nam * 'dtrm intro_pattern_expr CAst.t option) option
+ ('nam * 'dtrm intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 47f1d3bf66..871f418915 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -444,11 +444,11 @@ let intern_red_expr ist = function
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
-let intern_in_hyp_as ist lf (id,ipat) =
- (intern_hyp ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
let intern_hyp_list ist = List.map (intern_hyp ist)
+let intern_in_hyp_as ist lf (idl,ipat) =
+ (intern_hyp ist idl, Option.map (intern_intro_pattern lf ist) ipat)
+
let intern_inversion_strength lf ist = function
| NonDepInversion (k,idl,ids) ->
NonDepInversion (k,intern_hyp_list ist idl,
@@ -527,7 +527,7 @@ let rec intern_atomic lf ist x =
TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
| 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)
+ List.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings_arg ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3d734d3a66..db86567114 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
(k,(make ?loc f))) cb
in
let sigma,tac = match cl with
- | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
- | Some cl ->
- let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
- sigma, Tactics.apply_delayed_in a ev id l cl in
+ | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
+ | cl ->
+ let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in
+ sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in
Tacticals.New.tclWITHHOLES ev tac sigma
end
end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ec44ae4698..5f09666778 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -128,7 +128,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Basic tactics *)
| TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
| TacApply (a,ev,cb,cl) ->
- TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
+ TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,
+ List.map (on_snd (Option.map (subst_intro_pattern subst))) cl)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_glob_with_bindings_arg subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e3369bc9be..8b38bc1b0a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2635,7 +2635,7 @@ let assert_as first hd ipat t =
(* apply in as *)
let general_apply_in ?(respect_opaque=false) with_delta
- with_destruct with_evars id lemmas ipat =
+ with_destruct with_evars id lemmas ipat then_tac =
let tac (naming,lemma) tac id =
apply_in_delayed_once ~respect_opaque with_delta
with_destruct with_evars naming id lemma tac in
@@ -2653,7 +2653,8 @@ let general_apply_in ?(respect_opaque=false) with_delta
List.map (fun lem -> (NamingMustBe (CAst.make id),lem)) first, (naming,last)
in
(* We chain apply_in_once, ending with an intro pattern *)
- List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+ List.fold_right tac lemmas_target
+ (tac last_lemma_target (fun id -> Tacticals.New.tclTHEN (ipat_tac id) then_tac)) id
end
(*
@@ -2666,10 +2667,10 @@ let general_apply_in ?(respect_opaque=false) with_delta
let apply_in simple with_evars id lemmas ipat =
let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
- general_apply_in simple simple with_evars id lemmas ipat
+ general_apply_in simple simple with_evars id lemmas ipat Tacticals.New.tclIDTAC
-let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
+let apply_delayed_in simple with_evars id lemmas ipat then_tac =
+ general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat then_tac
(*****************************)
(* Tactics abstracting terms *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 54c781af5c..0fd2f1253f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -233,7 +233,7 @@ val apply_in :
val apply_delayed_in :
advanced_flag -> evars_flag -> Id.t ->
(clear_flag * delayed_open_constr_with_bindings CAst.t) list ->
- intro_pattern option -> unit Proofview.tactic
+ intro_pattern option -> unit Proofview.tactic -> unit Proofview.tactic
(** {6 Elimination tactics. } *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index e1df9ba84a..8c4b567106 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -530,6 +530,16 @@ rewrite H0.
change (x+0=0).
Abort.
+Goal (forall x y, x <= y -> y + x = 0 /\ True) -> exists x y, (x <= 0 -> y <= 1 -> 0 = 0 /\ 1 = 0).
+intros.
+do 2 eexists.
+intros.
+eapply H in H0 as (H0,_), H1 as (H1,_).
+split.
+- exact H0.
+- exact H1.
+Qed.
+
(* 2nd order apply used to have delta on local definitions even though
it does not have delta on global definitions; keep it by
compatibility while finding a more uniform way to proceed. *)
@@ -582,3 +592,22 @@ intros. eexists ?[p]. split. rewrite H.
reflexivity.
exact H0.
Qed.
+
+(* apply and side conditions: we check that apply in iterates only on
+ the main subgoals *)
+
+Goal (forall x, x=0 -> x>=0 -> x<=0 \/ x<=1) -> 0>=0 -> 1>=0 -> 1=0 -> True.
+intros f H H0 H1.
+apply f in H as [], H0 as [].
+1-3: change (0 <= 0) in H.
+4-6: change (0 <= 1) in H.
+1: change (1 <= 0) in H0.
+4: change (1 <= 0) in H0.
+2: change (1 <= 1) in H0.
+5: change (1 <= 1) in H0.
+1-2,4-5: exact I.
+1,2: exact H1.
+change (0 >= 0) in H.
+change (1 >= 0) in H0.
+exact (eq_refl 0).
+Qed.
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 9ca38d64df..69758b3f37 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -106,7 +106,7 @@ let apply adv ev cb cl =
| None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
| Some (id, cl) ->
let cl = Option.map mk_intro_pattern cl in
- Tactics.apply_delayed_in adv ev id cb cl
+ Tactics.apply_delayed_in adv ev id cb cl Tacticals.New.tclIDTAC
let mk_destruction_arg = function
| ElimOnConstr c ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:41:51 +0000