Restructuration fonctions de réécriture depuis égalité dépendante

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

2 files changed, 21 insertions, 16 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fd90a0a49..1346eef47 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -19,22 +19,24 @@ open Extraargs
 open Equality
 
 TACTIC EXTEND Rewrite
-  [ "Rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c]
+| [ "Rewrite" orient(b) constr_with_bindings(c) ] ->
+    [general_rewrite_bindings b c]
 END
 
 TACTIC EXTEND RewriteIn
- [ "Rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
- [general_rewrite_in b h c]
+| [ "Rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
+    [general_rewrite_bindings_in b h c]
 END
 
 let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
 
 TACTIC EXTEND Replace
-  [ "Replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ]
+| [ "Replace" constr(c1) "with" constr(c2) ] ->
+    [ replace c1 c2 ]
 END
 
 TACTIC EXTEND ReplaceIn
-  [ "Replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
+| [ "Replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
     [ replace_in h c1 c2 ]
 END
 
@@ -93,10 +95,13 @@ TACTIC EXTEND ConditionalRewriteIn
 END
 
 TACTIC EXTEND DependentRewrite
-| [ "Dependent" "Rewrite" orient(b) hyp(id) ] -> [ substHypInConcl b id ]
-| [ "CutRewrite" orient(b) constr(eqn) ] -> [ substConcl b eqn ]
+| [ "Dependent" "Rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+END
+
+TACTIC EXTEND CutRewrite
+| [ "CutRewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
 | [ "CutRewrite" orient(b) constr(eqn) "in" hyp(id) ]
-      -> [ substHyp b eqn id ]
+      -> [ cutRewriteInHyp b eqn id ]
 END
 
 (* Contradiction *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b09703369..94ec50e9d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -305,16 +305,16 @@ let remember_first_eq id x = if !x = None then x := Some id
 
 let projectAndApply thin id eqname names depids gls =
   let env = pf_env gls in
-  let clearer id =
-    if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in
-  let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id onConcl)) (clearer id) in
-  let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id onConcl)) (clearer id) in
+  let subst_hyp l2r id =
+    tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
+      (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
+  in
   let substHypIfVariable tac id gls =
     let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in
     match (kind_of_term t1, kind_of_term t2) with
-      | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
-      | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
-      | _ -> tac id gls
+    | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 gls
+    | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls
+    | _ -> tac id gls
   in
   let deq_trailer id neqns =
     tclTHENSEQ 
@@ -324,7 +324,7 @@ let projectAndApply thin id eqname names depids gls =
 	   (intro_move idopt None)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
-	   (tclTRY (onLastHyp (substHypIfVariable subst_hyp_RL))))
+	   (tclTRY (onLastHyp (substHypIfVariable (subst_hyp false)))))
 	 names);
        (if names = [] then clear [id] else tclIDTAC)]
   in