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

6 files changed, 9 insertions, 1 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7aadc305d3..6a4ee990d0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -127,8 +127,11 @@ GEXTEND Gram
          <:ast< (DISJPATTERN ($LIST $tc)) >>
       | "("; tc = LIST1 intropattern SEP "," ; ")" -> 
          <:ast< (CONJPATTERN ($LIST $tc)) >>
+      | IDENT "_" -> 
+	 <:ast< (WILDCAR) >>
       | id = identarg                   -> 
-         <:ast< (IDENTIFIER $id) >> ] ]
+         <:ast< (IDENTIFIER $id) >> 
+      ] ]
   ;
   intropattern:
     [ [   tc = LIST1 simple_intropattern -> 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index b6867ef89f..43bd3c7497 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -348,6 +348,7 @@ let ast_of_cvt_bind f = function
   | (Com,c)     -> ope ("BINDING", [ope ("COMMAND",[(f c)])])
 
 let rec ast_of_cvt_intro_pattern = function
+  | WildPat   -> ope ("WILDCAR",[])
   | IdPat id  -> nvar (string_of_id id) 
   | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
   | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index cf92c41e6d..bf8deb53a5 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -110,6 +110,7 @@ and tactic_arg =
   | Intropattern   of intro_pattern
 
 and intro_pattern =
+  | WildPat
   | IdPat   of identifier
   | DisjPat of intro_pattern list
   | ConjPat of intro_pattern list
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index a09504b366..de2c155f07 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -142,6 +142,7 @@ and tactic_arg =
   | Intropattern   of intro_pattern
 
 and intro_pattern =
+  | WildPat
   | IdPat   of identifier
   | DisjPat of intro_pattern list
   | ConjPat of intro_pattern list
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index b5f4d88f02..cf120ecdc6 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -1120,6 +1120,7 @@ and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function
 
 (* Interprets the patterns of Intro *)
 and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
+  | Node(_,"WILDCAR", []) -> WildPat
   | Node(_,"IDENTIFIER", [Nvar(loc,s)]) ->
     IdPat (id_of_Identifier (unvarg (val_interp
       (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s)))))
diff --git a/tactics/elim.ml b/tactics/elim.ml
index c61cdb0774..ffe2ff0715 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