From 3b83b311798f0d06444e1994602e0b531e207ef5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 6 Jun 2014 15:21:37 +0200
Subject: Moving the [split] tactic out of the AST.

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/tacinterp.ml')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ca9aabab..1ca63b53a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       end
 
   (* Constructors *)
-  | TacSplit (ev,_,bll) ->
+  | TacSplit (ev,bll) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-- 
cgit v1.2.3