Ajout 'dependent rewrite in'

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

1 files changed, 5 insertions, 6 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1346eef47..92f964cb8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -84,24 +84,23 @@ END
 let h_injHyp id = h_injection (Some id)
 
 TACTIC EXTEND ConditionalRewrite
-  [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ]
+| [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ]
     -> [ conditional_rewrite b (snd tac) c ]
-END
-
-TACTIC EXTEND ConditionalRewriteIn
-  [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c)
+| [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c)
     "in" hyp(h) ]
     -> [ conditional_rewrite_in b h (snd tac) c ]
 END
 
 TACTIC EXTEND DependentRewrite
 | [ "Dependent" "Rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+| [ "Dependent" "Rewrite" orient(b) constr(c) "in" hyp(id) ]
+    -> [ rewriteInHyp b c id ]
 END
 
 TACTIC EXTEND CutRewrite
 | [ "CutRewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
 | [ "CutRewrite" orient(b) constr(eqn) "in" hyp(id) ]
-      -> [ cutRewriteInHyp b eqn id ]
+    -> [ cutRewriteInHyp b eqn id ]
 END
 
 (* Contradiction *)