diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 18:05:26 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 18:05:26 +0000 |
| commit | 6401e75b74e02078d0ac3e94ba9c336c0a6a834b (patch) | |
| tree | d9ae88eafdc8466231eda7d72c75ace4f2ee456c /tactics | |
| parent | 3725135942a9778cbc741602dc6ecba23dde46f8 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elim.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |