From 9dec278bb1af17f30021bf0bb04f21682d1f0a3c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2007 16:35:07 +0000
Subject: 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
---
 contrib/interface/xlate.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

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
-- 
cgit v1.2.3