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

3 files changed, 10 insertions, 17 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index fb71288a97..8f880a767e 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -685,8 +685,8 @@ and ct_TACTIC_COM =
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
   | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
-  | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
-  | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
+  | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
+  | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE
   | CT_right of ct_SPEC_LIST
   | CT_ring of ct_FORMULA_LIST
   | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 5a7ccc26b1..064d20abd4 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1717,12 +1717,12 @@ and fTACTIC_COM = function
 | CT_rewrite_lr(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fNODE "rewrite_lr" 3
 | CT_rewrite_rl(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
-   fID_OPT x3;
+   fCLAUSE x3;
    fNODE "rewrite_rl" 3
 | CT_right(x1) ->
    fSPEC_LIST x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 21138c85e4..b9cd78e0b2 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