From 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 00:12:19 +0200
Subject: Removing "rename" from the tactic AST.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e1d4809609..379dd59d39 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -156,9 +156,6 @@ type 'a gen_atomic_tactic_expr =
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
 
-  (* Context management *)
-  | TacRename of ('nam *'nam) list
-
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
-- 
cgit v1.2.3