aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a480f6de6..71b3c0045 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,12 +563,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
let replace c2 c1 = multi_replace onConcl c2 c1 false None
-let replace_in id c2 c1 = multi_replace (onHyp id) c2 c1 false None
-
let replace_by c2 c1 tac = multi_replace onConcl c2 c1 false (Some tac)
-let replace_in_by id c2 c1 tac = multi_replace (onHyp id) c2 c1 false (Some tac)
-
let replace_in_clause_maybe_by c2 c1 cl tac_opt =
multi_replace cl c2 c1 false tac_opt