aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_tactic.ml421
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacinterp.ml17
-rw-r--r--plugins/ltac/tacsubst.ml4
6 files changed, 34 insertions, 22 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index c6a3beb896..83bfd0233a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -538,16 +538,27 @@ GEXTEND Gram
TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
| IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None))
| IDENT "pose"; b = constr; na = as_name ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
+ | IDENT "epose"; (id,b) = bindings_with_parameters ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None))
+ | IDENT "epose"; b = constr; na = as_name ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
| IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None))
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
+ | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None))
+ | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None))
| IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
p = clause_dft_all ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e))
+ | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
+ p = clause_dft_all ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 22ecf61aa2..4e254ea766 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -786,11 +786,11 @@ type 'a extra_genarg_printer =
pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
l
)
- | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
- hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
- | TacLetTac (na,c,cl,b,e) ->
+ | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
+ hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ | TacLetTac (ev,na,c,cl,b,e) ->
hov 1 (
- (if b then primitive "set" else primitive "remember") ++
+ primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
(if b then pr_pose pr.pr_constr pr.pr_lconstr na c
else pr_pose_as_style pr.pr_constr na c) ++
pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 11e7278d92..b78dc37426 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -144,7 +144,7 @@ type 'a gen_atomic_tactic_expr =
evars_flag * bool * 'tacexpr option option *
'dtrm intro_pattern_expr located option * 'trm
| TacGeneralize of ('trm with_occurrences * Name.t) list
- | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
+ | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
intro_pattern_naming_expr located option
(* Derived basic tactics *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 734ce46e48..2dc3bb3786 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -497,9 +497,9 @@ let rec intern_atomic lf ist x =
TacGeneralize (List.map (fun (c,na) ->
intern_constr_with_occurrences ist c,
intern_name lf ist na) cl)
- | TacLetTac (na,c,cls,b,eqpat) ->
+ | TacLetTac (ev,na,c,cls,b,eqpat) ->
let na = intern_name lf ist na in
- TacLetTac (na,intern_constr ist c,
+ TacLetTac (ev,na,intern_constr ist c,
(clause_app (intern_hyp_location ist) cls),b,
(Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d4ed770153..6b0914ff95 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1751,36 +1751,37 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacGeneralize cl)
(Tactics.generalize_gen cl)) sigma
end }
- | TacLetTac (na,c,clp,b,eqpat) ->
+ | TacLetTac (ev,na,c,clp,b,eqpat) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let clp = interp_clause ist env sigma clp in
let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
- if Locusops.is_nowhere clp then
+ if Locusops.is_nowhere clp (* typically "pose" *) then
(* We try to fully-typecheck the term *)
- let (sigma,c_interp) = interp_constr ist env sigma c in
+ let flags = open_constr_use_classes_flags () in
+ let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
let let_tac b na c cl eqpat =
let id = Option.default (Loc.tag IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
Tactics.letin_tac with_eq na c None cl
in
let na = interp_name ist env sigma na in
- Tacticals.New.tclWITHHOLES false
+ Tacticals.New.tclWITHHOLES ev
(name_atomic ~env
- (TacLetTac(na,c_interp,clp,b,eqpat))
+ (TacLetTac(ev,na,c_interp,clp,b,eqpat))
(let_tac b na c_interp clp eqpat)) sigma
else
(* We try to keep the pattern structure as much as possible *)
let let_pat_tac b na c cl eqpat =
let id = Option.default (Loc.tag IntroAnonymous) eqpat in
let with_eq = if b then None else Some (true,id) in
- Tactics.letin_pat_tac with_eq na c cl
+ Tactics.letin_pat_tac ev with_eq na c cl
in
let (sigma',c) = interp_pure_open_constr ist env sigma c in
name_atomic ~env
- (TacLetTac(na,c,clp,b,eqpat))
- (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
+ (TacLetTac(ev,na,c,clp,b,eqpat))
+ (Tacticals.New.tclWITHHOLES ev
(let_pat_tac b (interp_name ist env sigma na)
(sigma,c) clp eqpat) sigma')
end }
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 1ae792971c..f5e6f05cee 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -151,8 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
subst_glob_constr subst c)
| TacGeneralize cl ->
TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
- | TacLetTac (id,c,clp,b,eqpat) ->
- TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
+ | TacLetTac (ev,id,c,clp,b,eqpat) ->
+ TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat)
(* Derived basic tactics *)
| TacInductionDestruct (isrec,ev,(l,el)) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 21:53:56 +0000