aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--doc/refman/RefMan-tac.tex5
-rw-r--r--grammar/q_coqast.ml46
-rw-r--r--intf/tacexpr.mli3
-rw-r--r--parsing/g_tactic.ml413
-rw-r--r--printing/pptactic.ml5
-rw-r--r--tactics/hiddentac.ml15
-rw-r--r--tactics/hiddentac.mli7
-rw-r--r--tactics/tacinterp.ml16
9 files changed, 45 insertions, 27 deletions
diff --git a/CHANGES b/CHANGES
index 91e5a33b0..731083273 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ Tactics
- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
or "induction" to make it generate equations in the spirit of "case_eq".
The former syntax "_eqn" is discontinued.
+- The name of the hypothesis introduced by tactic "remember" can be
+ set via the new syntax "remember t as x eqn:H" (wish #2489).
Program
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 505db64d0..124036afa 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -626,6 +626,11 @@ Section~\ref{Occurrences clauses}.
This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a
logical (Leibniz's) equality instead of a local definition.
+\item {\tt remember {\term} {\tt as} {\ident} {\tt eqn:\ident}}
+
+ This behaves as {\tt remember {\term} {\tt as} {\ident}}, except
+ that the name of the generated equality is also given.
+
\item {\tt remember {\term} {\tt as} {\ident} in {\occgoalset}}
This is a more general form of {\tt remember} that remembers the
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3c646c03a..336468d12 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -347,11 +347,13 @@ let rec mlexpr_of_atomic_tactic = function
(mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >>
| Tacexpr.TacGeneralizeDep c ->
<:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
- | Tacexpr.TacLetTac (na,c,cl,b) ->
+ | Tacexpr.TacLetTac (na,c,cl,b,e) ->
let na = mlexpr_of_name na in
let cl = mlexpr_of_clause_pattern cl in
<:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$
- $mlexpr_of_bool b$ >>
+ $mlexpr_of_bool b$
+ (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) e)
+ >>
(* Derived basic tactics *)
| Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index a70ed47d4..ebff7b64c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -113,7 +113,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
| TacAssert of 'tac option * intro_pattern_expr located option * 'constr
| TacGeneralize of ('constr with_occurrences * name) list
| TacGeneralizeDep of 'constr
- | TacLetTac of name * 'constr * 'id clause_expr * letin_flag
+ | TacLetTac of name * 'constr * 'id clause_expr * letin_flag *
+ intro_pattern_expr located option
(* Derived basic tactics *)
| TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 202512a41..f24c9af63 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -541,15 +541,16 @@ GEXTEND Gram
TacMutualCofix (false,id,List.map mk_cofix_tac fd)
| IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacLetTac (Names.Name id,b,Locusops.nowhere,true)
+ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)
| IDENT "pose"; b = constr; na = as_name ->
- TacLetTac (na,b,Locusops.nowhere,true)
+ TacLetTac (na,b,Locusops.nowhere,true,None)
| IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacLetTac (Names.Name id,c,p,true)
+ TacLetTac (Names.Name id,c,p,true,None)
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
- TacLetTac (na,c,p,true)
- | IDENT "remember"; c = constr; na = as_name; p = clause_dft_all ->
- TacLetTac (na,c,p,false)
+ TacLetTac (na,c,p,true,None)
+ | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
+ p = clause_dft_all ->
+ TacLetTac (na,c,p,false,e)
(* Begin compatibility *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e1575eab7..f89877e00 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -697,12 +697,13 @@ and pr_atom1 = function
| TacGeneralizeDep c ->
hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
pr_constrarg c)
- | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere ->
+ | TacLetTac (na,c,cl,true,_) when cl = Locusops.nowhere ->
hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
- | TacLetTac (na,c,cl,b) ->
+ | TacLetTac (na,c,cl,b,e) ->
hov 1 ((if b then str "set" else str "remember") ++
(if b then pr_pose pr_lconstr else pr_pose_as_style)
pr_constr na c ++
+ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
pr_clauses (Some b) pr_ident cl)
(* | TacInstantiate (n,c,ConclLocation ()) ->
hov 1 (str "instantiate" ++ spc() ++
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 20b70cef4..990043ada 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -63,12 +63,15 @@ let h_generalize cl =
cl)
let h_generalize_dep c =
abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
-let h_let_tac b na c cl =
- let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
- abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl)
-let h_let_pat_tac b na c cl =
- let with_eq = if b then None else Some (true,(Loc.ghost,IntroAnonymous)) in
- abstract_tactic (TacLetTac (na,snd c,cl,b))
+let h_let_tac b na c cl eqpat =
+ let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+ let with_eq = if b then None else Some (true,id) in
+ abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
+ (letin_tac with_eq na c None cl)
+let h_let_pat_tac b na c cl eqpat =
+ let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+ let with_eq = if b then None else Some (true,id) in
+ abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
(letin_pat_tac with_eq na c None cl)
(* Derived basic tactics *)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 3028d3a1e..12791dfb5 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -57,10 +57,11 @@ val h_cut : constr -> tactic
val h_generalize : constr list -> tactic
val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic
val h_generalize_dep : constr -> tactic
-val h_let_tac : letin_flag -> name -> constr ->
- Locus.clause -> tactic
+val h_let_tac : letin_flag -> name -> constr -> Locus.clause ->
+ intro_pattern_expr located option -> tactic
val h_let_pat_tac : letin_flag -> name -> evar_map * constr ->
- Locus.clause -> tactic
+ Locus.clause -> intro_pattern_expr located option ->
+ tactic
(** Derived basic tactics *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3eddb1aae..d7ac1e66e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,10 +718,11 @@ let rec intern_atomic lf ist x =
intern_constr_with_occurrences ist c,
intern_name lf ist na) cl)
| TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
- | TacLetTac (na,c,cls,b) ->
+ | TacLetTac (na,c,cls,b,eqpat) ->
let na = intern_name lf ist na in
TacLetTac (na,intern_constr ist c,
- (clause_app (intern_hyp_location ist) cls),b)
+ (clause_app (intern_hyp_location ist) cls),b,
+ (Option.map (intern_intro_pattern lf ist) eqpat))
(* Automation tactics *)
| TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
@@ -2398,18 +2399,18 @@ and interp_atomic ist gl tac =
tclTHEN
(tclEVARS sigma)
(h_generalize_dep c_interp)
- | TacLetTac (na,c,clp,b) ->
+ | TacLetTac (na,c,clp,b,eqpat) ->
let clp = interp_clause ist gl clp in
if clp = Locusops.nowhere then
- (* We try to fully-typechect the term *)
+ (* We try to fully-typecheck the term *)
let (sigma,c_interp) = pf_interp_constr ist gl c in
tclTHEN
(tclEVARS sigma)
- (h_let_tac b (interp_fresh_name ist env na) c_interp clp)
+ (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
else
(* We try to keep the pattern structure as much as possible *)
h_let_pat_tac b (interp_fresh_name ist env na)
- (interp_pure_open_constr ist env sigma c) clp
+ (interp_pure_open_constr ist env sigma c) clp eqpat
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
@@ -2854,7 +2855,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacGeneralize cl ->
TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
| TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
- | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
+ | TacLetTac (id,c,clp,b,eqpat) ->
+ TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
(* Automation tactics *)
| TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 11:56:44 +0000