Permalink
Browse files

The tactic remember now accepts a final eqn:H option (grant wish #2489)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent f3870c9 commit 9e04031196175111302681d96d975804bd7e1850 letouzey committed Jul 9, 2012
Showing with 45 additions and 27 deletions.
  1. +2 −0 CHANGES
  2. +5 −0 doc/refman/RefMan-tac.tex
  3. +4 −2 grammar/q_coqast.ml4
  4. +2 −1 intf/tacexpr.mli
  5. +7 −6 parsing/g_tactic.ml4
  6. +3 −2 printing/pptactic.ml
  7. +9 −6 tactics/hiddentac.ml
  8. +4 −3 tactics/hiddentac.mli
  9. +9 −7 tactics/tacinterp.ml
View
2 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
View
5 doc/refman/RefMan-tac.tex
@@ -626,6 +626,11 @@ \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
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
View
6 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) ->
View
3 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
View
13 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; ":=";
View
5 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() ++
View
15 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 *)
View
7 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 *)
View
16 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)

0 comments on commit 9e04031

Please sign in to comment.