+ 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

15 files changed, 153 insertions, 29 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 335afddd22..fb71288a97 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 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;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 4556d818e0..da87086e29 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"
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9bb8d07541..e8829acbab 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -363,8 +363,8 @@ GEXTEND Gram
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
-      | IDENT "destruct"; c = induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewDestruct (c,el,ids)
+      | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; 
+	  el = OPT eliminator -> TacNewDestruct (lc,el,ids)
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9ec4dfd03c..a90e001f5d 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -691,7 +691,8 @@ and pr_atom1 env = function
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (h,e,ids) ->
       hov 1 (str "destruct" ++ spc () ++
-             pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++
+             prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ 
+	     pr_with_names ids ++
              pr_opt (pr_eliminator env) e)
   | TacDoubleInduction (h1,h2) ->
       hov 1
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f33c5a9559..b05895666f 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -330,7 +330,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_intro_pattern ids in
-      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
+      <:expr< Tacexpr.TacNewDestruct $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
 
   (* Context management *)
   | Tacexpr.TacClear (b,l) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 42a5d5cbe2..ea7c49f2bc 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -141,7 +141,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option
       * intro_pattern_expr
   | TacSimpleDestruct of quantified_hypothesis
-  | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
+  | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option
       * intro_pattern_expr
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6b67dd4966..0727d8ce46 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -128,9 +128,10 @@ let rewriteRL_clause = function
 (* eq,sym_eq : equality on Type and its symmetry theorem
    c2 c1 : c1 is to be replaced by c2
    unsafe : If true, do not check that c1 and c2 are convertible
+   tac : Used to prove the equality c1 = c2 
    gl : goal *)
 
-let abstract_replace clause c2 c1 unsafe gl =
+let abstract_replace clause c2 c1 unsafe tac gl =
   let t1 = pf_type_of gl c1 
   and t2 = pf_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
@@ -142,14 +143,32 @@ let abstract_replace clause c2 c1 unsafe gl =
 	tclTHEN 
 	  (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
 	  (clear [id]));
-       tclORELSE assumption 
-	(tclTRY (tclTHEN (apply sym) assumption))] gl
+       tclFIRST
+	 [assumption;
+	  tclTHEN (apply sym) assumption;
+	  tclTRY (tclCOMPLETE tac)
+	 ]
+      ] gl
   else
     error "terms does not have convertible types"
 
-let replace c2 c1 gl = abstract_replace None c2 c1 false gl
 
-let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false gl
+let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl
+
+let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl
+
+let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl
+
+let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl
+
+
+let new_replace c2 c1 id tac_opt gl = 
+  let tac = 
+    match tac_opt with 
+      | Some tac -> tac 
+      | _ -> tclIDTAC
+  in
+  abstract_replace id c2 c1 false tac gl
 
 (* End of Eduardo's code. The rest of this file could be improved
    using the functions match_with_equation, etc that I defined
diff --git a/tactics/equality.mli b/tactics/equality.mli
index fc7c3828ea..7632fd36bd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -49,7 +49,9 @@ val conditional_rewrite_in :
 
 val replace    : constr -> constr -> tactic
 val replace_in : identifier -> constr -> constr -> tactic
-
+val replace_by : constr -> constr -> tactic -> tactic 
+val replace_in_by : identifier -> constr -> constr -> tactic -> tactic 
+val new_replace : constr -> constr -> identifier option -> tactic option -> tactic
 val discr        : identifier -> tactic
 val discrConcl   : tactic
 val discrClause  : clause -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7aae9f5224..97aeedc6b3 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -32,16 +32,83 @@ END
 
 let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
 
+(* Julien: Mise en commun des differentes version de replace with in by 
+   TODO: améliorer l'affichage et deplacer dans extraargs
+
+*)
+
+
+let pr_by_arg_tac prc _ _ opt_c = 
+  match opt_c with 
+    | None -> mt ()
+    | Some c -> spc () ++ hov 2 (str "by" ++ spc ()  )
+
+(* Julien Forest: on voudrait pouvoir passer la loc mais je 
+n'ai pas reussi 
+*)
+
+let pr_in_arg_hyp  = 
+fun prc _ _ opt_c->
+  match opt_c with 
+    | None -> mt ()
+    | Some c -> 
+	spc () ++ hov 2 (str "by" ++ spc () ++ 
+			   Pptactic.pr_or_var (fun _ -> mt ()) 
+			   (ArgVar(Util.dummy_loc,c))
+			)
+
+
+
+
+ARGUMENT EXTEND by_arg_tac
+  TYPED AS tactic_opt
+  PRINTED BY pr_by_arg_tac
+| [ "by" tactic(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+ 
+ARGUMENT EXTEND in_arg_hyp
+  TYPED AS ident_opt
+  PRINTED BY pr_in_arg_hyp
+| [ "in" int_or_var(c) ] -> 
+    [ match c with
+	| ArgVar(_,c) ->  Some (c)
+	| _ -> Util.error "in must be used with an identifier" 
+    ]
+| [ ] -> [ None ]
+END
+
+TACTIC EXTEND replace 
+| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp)  by_arg_tac(tac)  ] ->
+    [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac)  ]
+END
+
+(* Julien:
+  old version  
+
 TACTIC EXTEND replace
 | [ "replace" constr(c1) "with" constr(c2) ] ->
     [ replace c1 c2 ]
 END
 
+TACTIC EXTEND replace_by
+|  [ "replace" constr(c1) "with" constr(c2) "by" tactic(tac) ] ->
+    [ replace_by c1 c2 (snd tac)  ]
+ 
+END
+
 TACTIC EXTEND replace_in
 | [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
     [ replace_in h c1 c2 ]
 END
 
+TACTIC EXTEND replace_in_by
+| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) "by" tactic(tac) ] ->
+    [ replace_in_by h c1 c2 (snd tac) ]
+END
+
+*)
+
 TACTIC EXTEND replace_term_left
   [ "replace" "->" constr(c)  ] -> [ replace_term_left c ]
 END
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 9431a68715..0e47cf4f37 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -18,3 +18,23 @@ val h_injHyp : quantified_hypothesis -> tactic
 val h_rewriteLR : constr -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic
+
+
+
+(* Julien: Mise en commun des differentes version de replace with in by 
+   TODO:  deplacer dans extraargs
+
+*)
+
+
+val rawwit_in_arg_hyp:  identifier option Tacexpr.raw_abstract_argument_type
+val in_arg_hyp: identifier option Pcoq.Gram.Entry.e
+
+
+
+val rawwit_by_arg_tac :
+  (Tacexpr.raw_tactic_expr option, Topconstr.constr_expr,
+   Tacexpr.raw_tactic_expr)
+  Genarg.abstract_argument_type
+  
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 00e780ad30..15bea4bb3a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -60,7 +60,7 @@ val h_new_induction   :
   constr induction_arg list -> constr with_bindings option ->
   intro_pattern_expr -> tactic
 val h_new_destruct    :
-  constr induction_arg -> constr with_bindings option -> 
+  constr induction_arg list -> constr with_bindings option -> 
   intro_pattern_expr -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 12c319b947..ee4e61179b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -677,7 +677,7 @@ let rec intern_atomic lf ist x =
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
-      TacNewDestruct (intern_induction_arg ist c,
+      TacNewDestruct (List.map (intern_induction_arg ist) c,
                option_app (intern_constr_with_bindings ist) cbo,
 	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
@@ -1780,7 +1780,7 @@ and interp_atomic ist gl = function
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) -> 
-      h_new_destruct (interp_induction_arg ist gl c)
+      h_new_destruct (List.map (interp_induction_arg ist gl) c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
@@ -2037,7 +2037,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
                option_app (subst_raw_with_bindings subst) cbo, ids)
   | TacSimpleDestruct h as x -> x
   | TacNewDestruct (c,cbo,ids) ->
-      TacNewDestruct (subst_induction_arg subst c,
+      TacNewDestruct (List.map (subst_induction_arg subst) c,  (* Julien F. est-ce correct? *)
                option_app (subst_raw_with_bindings subst) cbo, ids)
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0f061fd76f..bddb82c54c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2058,7 +2058,7 @@ let new_induct_destruct_l isrec lc elim names =
       
 
 let new_induct = new_induct_destruct_l true
-let new_destruct c = new_induct_destruct_l false [c]
+let new_destruct c = new_induct_destruct_l false c
 
 (* The registered tactic, which calls the default elimination
  * if no elimination constant is provided. *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c6dbc1be92..1c7967e10a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -235,7 +235,7 @@ val general_case_analysis : constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
-val new_destruct : constr induction_arg -> constr with_bindings option ->
+val new_destruct : constr induction_arg list -> constr with_bindings option ->
   intro_pattern_expr -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)