From eee66457ddfd86c65cc1287b4545f828bf43f2dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 29 Jun 2000 10:50:27 +0000
Subject: Rien

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index feb4bf69a6..9a03eca979 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1038,7 +1038,7 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) =
 	      [ central_intro (IBasedOn (recvarname,avoid)) destopt false;
 		central_intro (IBasedOn (hyprecname,avoid)) None false;
 		peel_tac c]
-    | DOP2 (Cast,c,t) -> peel_tac c
+    | DOP2 (Cast,c,_) -> peel_tac c
     | DOP2 (Prod,t,DLAM(na,c))
       -> tclTHEN (central_intro (IAvoid avoid) destopt false)
 	  (peel_tac c)
-- 
cgit v1.2.3