Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"

I wonder how many of us were aware of the existence of such syntax ;-)
Anyway, it is now subsumed by "rewrite by".

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

3 files changed, 0 insertions, 25 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 89a3704eef..3cf5cfd736 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -290,22 +290,9 @@ let general_multi_multi_rewrite with_evars l cl tac =
     | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
   in loop l
 
-(* Conditional rewriting, the success of a rewriting is related 
-   to the resolution of the conditions by a given tactic *)
-
-let conditional_rewrite lft2rgt tac (c,bl) = 
-  tclTHENSFIRSTn
-    (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false)
-    [|tclIDTAC|] (tclCOMPLETE tac)
-
 let rewriteLR = general_rewrite true all_occurrences
 let rewriteRL = general_rewrite false all_occurrences
 
-let conditional_rewrite_in lft2rgt id tac (c,bl) = 
-  tclTHENSFIRSTn
-    (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false)
-    [|tclIDTAC|] (tclCOMPLETE tac)
-
 (* Replacing tactics *)
 
 (* eq,sym_eq : equality on Type and its symmetry theorem
diff --git a/tactics/equality.mli b/tactics/equality.mli
index deb68aac8f..a52d064996 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -64,10 +64,6 @@ val general_multi_multi_rewrite :
   evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> 
   (tactic * conditions) option -> tactic
 
-val conditional_rewrite : orientation -> tactic -> open_constr with_bindings -> tactic
-val conditional_rewrite_in :
-  orientation -> identifier -> tactic -> open_constr with_bindings -> tactic
-
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
 val replace_in : identifier -> constr -> constr -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 6676b90acc..2b4b9cffe9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -134,14 +134,6 @@ END
 
 let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings)
 
-TACTIC EXTEND conditional_rewrite
-| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
-    -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ]
-| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
-    "in" hyp(h) ]
-    -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ]
-END
-
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
 | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]