From 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 23 Apr 2012 18:51:11 +0000
Subject: remove undocumented and scarcely-used tactic auto decomp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index cec6fd4199..b48605657a 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -177,7 +177,6 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   (* Automation tactics *)
   | TacTrivial of debug * 'constr list * string list option
   | TacAuto of debug * int or_var option * 'constr list * string list option
-  | TacDAuto of debug * int or_var option * int option * 'constr list
 
   (* Context management *)
   | TacClear of bool * 'id list
-- 
cgit v1.2.3