+ 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

3 files changed, 27 insertions, 12 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 335afddd2..fb71288a9 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -670,7 +670,7 @@ and ct_TACTIC_COM =
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
-  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
+  | CT_new_destruct of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
   | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
@@ -684,7 +684,7 @@ and ct_TACTIC_COM =
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
-  | CT_replace_with of ct_FORMULA * ct_FORMULA
+  | 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_right of ct_SPEC_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 88852aa59..5a7ccc26b 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;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4556d818e..da87086e2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -63,7 +63,7 @@ let coercion_description t = !coercion_description_holder t;;
 let set_coercion_description f =
  coercion_description_holder:=f; ();;
 
-let xlate_error s = failwith ("Translation error: " ^ s);;
+let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);;
 
 let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
 
@@ -957,10 +957,22 @@ and xlate_tac =
     | TacRight bindl -> CT_right (xlate_bindings bindl)
     | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
     | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
-    | TacExtend (_,"replace", [c1; c2]) ->
-     let c1 = xlate_formula (out_gen rawwit_constr c1) in
-     let c2 = xlate_formula (out_gen rawwit_constr c2) in
-     CT_replace_with (c1, c2)
+    | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) ->
+	let c1 = xlate_formula (out_gen rawwit_constr c1) in
+	let c2 = xlate_formula (out_gen rawwit_constr c2) in
+	let id_opt = 
+	  match out_gen Extratactics.rawwit_in_arg_hyp id_opt with 
+	  | None -> ctv_ID_OPT_NONE
+	  | Some id ->   ctf_ID_OPT_SOME (xlate_ident id)
+	in
+	let tac_opt = 
+	  match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
+	    | None -> CT_coerce_NONE_to_TACTIC_OPT  CT_none
+	    | Some tac ->
+		let tac =  xlate_tactic tac in
+		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
@@ -1157,8 +1169,8 @@ and xlate_tac =
     | TacDAuto (a, b) ->
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacNewDestruct(a,b,c) ->
-	CT_new_destruct
-	  (xlate_int_or_constr a, xlate_using b, 
+	CT_new_destruct (* Julien F. : est-ce correct *)
+	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
     | TacNewInduction(a,b,c) ->
 	CT_new_induction (* Pierre C. : est-ce correct *)
@@ -1195,6 +1207,7 @@ and xlate_tac =
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
     | TacExtend (_,id, l) ->
+	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
     | TacAlias _ -> xlate_error "Alias not supported"