Adding a syntax for "n-ary" rewrite:

 
 rewrite H, H'

means: rewrite H; rewrite H'. 

This should still be compatible with other "features" of rewrite: like
orientation, implicit arguments (t:=...), and "in" clause.  Concerning
the "in" clause, for the moment only one is allowed at the very end of
the tactic, and it applies to all the different rewrites that are
done. For instance, if someone _really_ wants to use all features at
the same time:

 rewrite H1 with (t:=u), <-H2, H3  in *

means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in *




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 48 insertions, 18 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 068110d74..9c81a1c3a 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 0ba9553ce..8dd168aad 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 3853a6d51..9d0cd28ff 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 b07213fe9..52b2e5f64 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 8c45d95b3..f99ce1a88 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 c5b7aeedf..4f94ba595 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 36fc99594..772f9cdc8 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 944b7710a..dc4b3822f 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