From 6401e75b74e02078d0ac3e94ba9c336c0a6a834b Mon Sep 17 00:00:00 2001
From: mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 12 Apr 2001 18:05:26 +0000
Subject: Ajout de _ dans les patterns d'intro

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

(limited to 'tactics')

diff --git a/tactics/elim.ml b/tactics/elim.ml
index c61cdb077..ffe2ff071 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -192,6 +192,7 @@ let rec intro_pattern p =
   let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
   and case_last  = (tclLAST_HYP h_simplest_case) in  
   match p with
+    | WildPat    -> (tclTHEN intro clear_last)
     | IdPat  id  -> intro_using_warning id
     | DisjPat l  -> (tclTHEN introf
                        (tclTHENS 
-- 
cgit v1.2.3