diff options
| author | herbelin | 2009-06-07 17:10:17 +0000 |
|---|---|---|
| committer | herbelin | 2009-06-07 17:10:17 +0000 |
| commit | 6a13615a1efa7e2e10ea8e7187d2bda0819fd1d5 (patch) | |
| tree | bb5a5d217f7eb0d2774c9159537176fa7ec5c03a /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 1 |
2 files changed, 4 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index e370b693f0..c0a3f2e770 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -256,7 +256,9 @@ GEXTEND Gram naming_intropattern: [ [ prefix = pattern_ident -> loc, IntroFresh prefix | "?" -> loc, IntroAnonymous - | id = ident -> loc, IntroIdentifier id ] ] + | id = ident -> loc, IntroIdentifier id + | "*" -> loc, IntroForthcoming true + | "**" -> loc, IntroForthcoming false ] ] ; intropattern_modifier: [ [ IDENT "_eqn"; diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 18322504e5..a494738f9c 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -75,6 +75,7 @@ let mlexpr_of_intro_pattern = function | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> + | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> | Genarg.IntroIdentifier id -> <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ -> |