+ destruct now works as induction on multiple arguments :

   destruct x y z using scheme
+ replace c1 with c2 <in hyp> has now a new optional argument <as tac> 
   replace c1 with c2 by tac tries to prove c2 = c1 with tac 
+ I've also factorize the code correspoing to replace in  extractactics



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

1 files changed, 5 insertions, 3 deletions

diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 88852aa59c..5a7ccc26b1 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1660,7 +1660,7 @@ and fTACTIC_COM = function
    fID x2;
    fNODE "move_after" 2
 | CT_new_destruct(x1, x2, x3) ->
-   fFORMULA_OR_INT x1;
+   (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *)
    fUSING x2;
    fINTRO_PATT_OPT x3;
    fNODE "new_destruct" 3
@@ -1708,10 +1708,12 @@ and fTACTIC_COM = function
 | CT_repeat(x1) ->
    fTACTIC_COM x1;
    fNODE "repeat" 1
-| CT_replace_with(x1, x2) ->
+| CT_replace_with(x1, x2,x3,x4) ->
    fFORMULA x1;
    fFORMULA x2;
-   fNODE "replace_with" 2
+   fID_OPT x3;
+   fTACTIC_OPT x4;
+   fNODE "replace_with" 4
 | CT_rewrite_lr(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;