From 0aba678e885fa53fa649de59eb1d06b4af3a847c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Dec 2015 20:42:07 +0100
Subject: Getting rid of the dynamic node of the tactic AST.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 73130d3804..ead221c5fb 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -209,7 +209,6 @@ constraint 'a = <
 (** Possible arguments of a tactic definition *)
 
 and 'a gen_tactic_arg =
-  | TacDynamic     of Loc.t * Dyn.t
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
-- 
cgit v1.2.3