aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacsubst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacsubst.ml')
-rw-r--r--tactics/tacsubst.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 36e0b4278..142a96445 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -178,9 +178,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
subst_glob_constr subst c, cl)
- (* Equivalence relations *)
- | TacSymmetry _ as x -> x
-
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
TacRewrite (ev,