aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml5
-rw-r--r--doc/refman/RefMan-tac.tex10
-rw-r--r--parsing/g_tactic.ml411
-rw-r--r--parsing/pptactic.ml10
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/equality.mli2
-rw-r--r--tactics/tacinterp.ml20
8 files changed, 48 insertions, 18 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 068110d747..9c81a1c3a2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1012,13 +1012,14 @@ and xlate_tac =
CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
in
CT_replace_with (c1, c2,cl,tac_opt)
- | TacRewrite(b,false,cbindl,cl) ->
+ | TacRewrite(false,[b,cbindl],cl) ->
let cl = xlate_clause cl
and c = xlate_formula (fst cbindl)
and bindl = xlate_bindings (snd cbindl) in
if b then CT_rewrite_lr (c, bindl, cl)
else CT_rewrite_rl (c, bindl, cl)
- | TacRewrite(b,true,cbindl,cl) -> xlate_error "TODO: erewrite"
+ | TacRewrite(false,_,cl) -> xlate_error "TODO: rewrite of several hyps at once"
+ | TacRewrite(true,_,cl) -> xlate_error "TODO: erewrite"
| TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
let t = out_gen rawwit_main_tactic t in
let b = out_gen Extraargs.rawwit_orient b in
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0ba9553ce4..8dd168aad2 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1728,6 +1728,16 @@ This happens if \term$_1$ does not occur in the goal.
\tacindex{rewrite <- \dots\ in}
Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
rewrite in \textit{clause} as explained above.
+
+\item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
+ Is equivalent to {\tt rewrite $\term_1$; \ldots; rewrite $\term_n$}.
+ Orientation {\tt ->} or {\tt <-} can be inserted before each term.
+
+\item {\tt rewrite $\term_1$, \ldots, $term_n$ in \textit{clause}}\\
+ Is equivalent to {\tt rewrite $\term_1$ in \textit{clause}; \ldots;
+ rewrite $\term_n$ in \textit{clause}}.
+ Orientation {\tt ->} or {\tt <-} can be inserted before each term.
+
\end{Variants}
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3853a6d51c..9d0cd28ff0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -317,6 +317,9 @@ GEXTEND Gram
rename :
[ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
;
+ rewriter :
+ [ [ b = orient; c = constr_with_bindings -> (b,c) ] ]
+ ;
simple_tactic:
[ [
(* Basic tactics *)
@@ -436,10 +439,10 @@ GEXTEND Gram
| IDENT "transitivity"; c = constr -> TacTransitivity c
(* Equality and inversion *)
- | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause ->
- TacRewrite (b,false,c,cl)
- | IDENT "erewrite"; b = orient; c = constr_with_bindings ; cl = clause ->
- TacRewrite (b,true,c,cl)
+ | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause ->
+ TacRewrite (false,l,cl)
+ | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause ->
+ TacRewrite (true,l,cl)
| IDENT "dependent"; k =
[ IDENT "simple"; IDENT "inversion" -> SimpleInversion
| IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index b07213fe98..52b2e5f647 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -824,9 +824,13 @@ and pr_atom1 = function
| TacTransitivity c -> str "transitivity" ++ pr_constrarg c
(* Equality and inversion *)
- | TacRewrite (b,ev,c,cl) ->
- hov 1 (str (if ev then "erewrite" else "rewrite") ++ pr_orient b ++
- spc() ++ pr_with_bindings c ++ pr_clauses pr_ident cl)
+ | TacRewrite (ev,l,cl) ->
+ hov 1 (str (if ev then "erewrite" else "rewrite") ++
+ prlist_with_sep
+ (fun () -> str ","++spc())
+ (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c)
+ l
+ ++ pr_clauses pr_ident cl)
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8c45d95b30..f99ce1a88c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -185,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacTransitivity of 'constr
(* Equality and inversion *)
- | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause
+ | TacRewrite of evars_flag * (bool * 'constr with_bindings) list * 'id gclause
| TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
(* For ML extensions *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c5b7aeedfb..4f94ba5953 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -166,6 +166,12 @@ let general_multi_rewrite l2r with_evars c cl =
(general_rewrite_ebindings l2r c with_evars)
do_hyps
+let rec general_multi_multi_rewrite with_evars l cl = match l with
+ | [] -> tclIDTAC
+ | (l2r,c)::l ->
+ tclTHEN (general_multi_rewrite l2r with_evars c cl)
+ (general_multi_multi_rewrite with_evars l cl)
+
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 36fc995940..772f9cdc8e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -48,6 +48,8 @@ val general_rewrite_in :
val general_multi_rewrite :
bool -> evars_flag -> constr with_ebindings -> clause -> tactic
+val general_multi_multi_rewrite :
+ evars_flag -> (bool * constr with_ebindings) list -> clause -> tactic
val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
val conditional_rewrite_in :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 944b7710a5..dc4b3822f7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -744,9 +744,11 @@ let rec intern_atomic lf ist x =
| TacTransitivity c -> TacTransitivity (intern_constr ist c)
(* Equality and inversion *)
- | TacRewrite (b,ev,c,cl) ->
- TacRewrite (b,ev,intern_constr_with_bindings ist c,
- clause_app (intern_hyp_location ist) cl)
+ | TacRewrite (ev,l,cl) ->
+ TacRewrite
+ (ev,
+ List.map (fun (b,c) -> (b,intern_constr_with_bindings ist c)) l,
+ clause_app (intern_hyp_location ist) cl)
| TacInversion (inv,hyp) ->
TacInversion (intern_inversion_strength lf ist inv,
intern_quantified_hypothesis ist hyp)
@@ -2158,9 +2160,9 @@ and interp_atomic ist gl = function
| TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
(* Equality and inversion *)
- | TacRewrite (b,ev,c,cl) ->
- Equality.general_multi_rewrite b ev
- (interp_constr_with_bindings ist gl c)
+ | TacRewrite (ev,l,cl) ->
+ Equality.general_multi_multi_rewrite ev
+ (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l)
(interp_clause ist gl cl)
| TacInversion (DepInversion (k,c,ids),hyp) ->
Inv.dinv k (option_map (pf_interp_constr ist gl) c)
@@ -2451,8 +2453,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
(* Equality and inversion *)
- | TacRewrite (b,ev,c,cl) ->
- TacRewrite (b,ev,subst_raw_with_bindings subst c,cl)
+ | TacRewrite (ev,l,cl) ->
+ TacRewrite (ev,
+ List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l,
+ cl)
| TacInversion (DepInversion (k,c,l),hyp) ->
TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
| TacInversion (NonDepInversion _,_) as x -> x
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 12:47:59 +0000