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

3 files changed, 20 insertions, 8 deletions

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