Extension syntaxique de rewrite in: au lieu de pouvoir faire

juste rewrite in <id>, on a maintenant rewrite in <clause>. 

Ainsi rewrite H in H1,H2 |- * === rewrite H in H1; rewrite H in H2; rewrite H

Pour l'instant rewrite H in * |- signifie: faire une fois 
"try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H
En particulier, n'echoue pour l'instant pas s'il n'y a rien a 
reecrire nulle part. 

NB: rewrite H in * === rewrite H in * |- * === rewrite H in * |- ; rewrite H

ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence. 
 Est-ce la bonne facon de faire ? 




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

1 files changed, 6 insertions, 13 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 21138c85e..b9cd78e0b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -978,19 +978,12 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,id_opt,tac_opt)
-    | TacExtend (_,"rewrite", [b; cbindl]) ->
-     let b = out_gen Extraargs.rawwit_orient b in
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
-     else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend (_,"rewrite_in", [b; cbindl; id]) ->
-     let b = out_gen Extraargs.rawwit_orient b in
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
-     if b then CT_rewrite_lr (c, bindl, id)
-     else CT_rewrite_rl (c, bindl, id)
+    | TacRewrite(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)
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in