Ajout 'replace in'

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

3 files changed, 21 insertions, 13 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1615d4b90..621781187 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -116,7 +116,11 @@ let rewriteRLin = general_rewrite_in false
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
   tclTHENSFIRSTn (general_rewrite_in lft2rgt id (c,bl))
     [|tclIDTAC|] (tclCOMPLETE tac)
-    
+
+let rewriteRL_clause = function
+  | None -> rewriteRL_bindings
+  | Some id -> rewriteRLin id
+
 (* Replacing tactics *)
 
 (* eqt,sym_eqt : equality on Type and its symmetry theorem
@@ -124,21 +128,24 @@ let conditional_rewrite_in lft2rgt id tac (c,bl) =
    unsafe : If true, do not check that c1 and c2 are convertible
    gl : goal *)
 
-let abstract_replace (eqt,sym_eqt) c2 c1 unsafe gl =
+let abstract_replace clause c2 c1 unsafe 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
-    let (e,sym) = (eqt,sym_eqt) in
-    (tclTHENLAST (elim_type (applist (e, [t1;c1;c2])))
-       (tclORELSE assumption 
-          (tclTRY (tclTHEN (apply sym) assumption)))) gl
+    let e = (build_coq_eqT_data ()).eq in
+    let sym = (build_coq_eqT_data ()).sym in
+    let eq = applist (e, [t1;c1;c2]) in
+    tclTHENS (cut eq)
+      [tclTHEN intro (onLastHyp (fun id -> 
+	tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id])));
+       tclORELSE assumption 
+	(tclTRY (tclTHEN (apply sym) assumption))] gl
   else
     error "terms does not have convertible types"
 
-let replace c2 c1 gl =
-  let eqT = (build_coq_eqT_data ()).eq in
-  let eqT_sym = (build_coq_eqT_data ()).sym in
-  abstract_replace (eqT,eqT_sym) c2 c1 false gl
+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
 
 (* 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 4e22d4141..271f0ebb2 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -39,7 +39,8 @@ val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
 
-val replace   : constr -> constr -> tactic
+val replace    : constr -> constr -> tactic
+val replace_in : identifier -> constr -> constr -> tactic
 
 type elimination_types =
   | Set_Type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 18b8f7326..22450cf98 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -34,8 +34,8 @@ TACTIC EXTEND Replace
 END
 
 TACTIC EXTEND ReplaceIn
-  [ "Replace" constr(c1) "with" constr(c2) "in" ident(h) ]
-  -> [ failwith "Replace in: TODO" ]
+  [ "Replace" constr(c1) "with" constr(c2) "in" ident(h) ] ->
+    [ replace_in h c1 c2 ]
 END
 
 TACTIC EXTEND Replacetermleft