+ 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

8 files changed, 120 insertions, 12 deletions

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. *)