From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 29 Feb 2016 12:11:52 +0100
Subject: Moving the "symmetry" tactic to TACTIC EXTEND.

---
 intf/tacexpr.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 52c07e089..3f1d0fd76 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -170,9 +170,6 @@ type 'a gen_atomic_tactic_expr =
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
 
-  (* Equivalence relations *)
-  | TacSymmetry of 'nam clause_expr
-
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
       (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
-- 
cgit v1.2.3