diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-07 17:10:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-07 17:10:17 +0000 |
| commit | 6a13615a1efa7e2e10ea8e7187d2bda0819fd1d5 (patch) | |
| tree | bb5a5d217f7eb0d2774c9159537176fa7ec5c03a /tactics/tacinterp.ml | |
| parent | 0329bbb517f0cb0f3707b209ef849d389cf870dc (diff) | |
- Added two new introduction patterns with the following temptative syntaxes:
- "*" implements Arthur Charguéraud's "introv"
- "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
library is really going anarchically (see a summary of the various
formulations of total order, dichotomy of order and decidability of
equality and in stdlib-project.tex in branch V8revised-theories).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cbc1c6ce2..c21a4c080 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -485,7 +485,7 @@ let rec intern_intro_pattern lf ist = function loc, IntroIdentifier (intern_ident lf ist id) | loc, IntroFresh id -> loc, IntroFresh (intern_ident lf ist id) - | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _) + | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x and intern_or_and_intro_pattern lf ist = @@ -1362,7 +1362,8 @@ let rec intropattern_ids (loc,pat) = match pat with | IntroIdentifier id -> [id] | IntroOrAndPattern ll -> List.flatten (List.map intropattern_ids (List.flatten ll)) - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> [] + | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ + | IntroForthcoming _ -> [] let rec extract_ids ids = function | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> @@ -1661,7 +1662,7 @@ let rec interp_intro_pattern ist gl = function loc, interp_intro_pattern_var loc ist (pf_env gl) id | loc, IntroFresh id -> loc, IntroFresh (interp_fresh_ident ist gl id) - | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _) + | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x and interp_or_and_intro_pattern ist gl = |