Moving the "symmetry" tactic to TACTIC EXTEND.

1 files changed, 0 insertions, 10 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d1a47dce5a..81fbcc6db6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1974,16 +1974,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end }
       end
 
-  (* Equivalence relations *)
-  | TacSymmetry c ->
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = project gl in
-        let cl = interp_clause ist env sigma c in
-        name_atomic ~env
-          (TacSymmetry cl)
-          (Tactics.intros_symmetry cl)
-      end }
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->