diff options
| author | glondu | 2007-07-09 15:10:16 +0000 |
|---|---|---|
| committer | glondu | 2007-07-09 15:10:16 +0000 |
| commit | 885aec961ab1a9e3c0c0bfde25742c2a43fddbc5 (patch) | |
| tree | 83a84ea0935288420121e34a09036ee517b7875d | |
| parent | 9c4f65ebe124d972ae1506e388bb206cb7298ce4 (diff) | |
More natural notation for intro pattern: @a -> ?a
Caveat about a slight loss of compatibility:
Some intro patterns don't need space between them. In particular
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9964 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 | ||||
| -rw-r--r-- | interp/genarg.ml | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 |
4 files changed, 9 insertions, 5 deletions
@@ -73,7 +73,11 @@ Tactics - The "with" arguments are now typed using informations from the current goal: allows support for coercions and more inference of implicit arguments. - Application of "f_equal"-style lemmas works better. -- New intro pattern "@A", which genererates a fresh name based on A. +- New intro pattern "?A", which genererates a fresh name based on A. + Caveat about a slight loss of compatibility: + Some intro patterns don't need space between them. In particular + intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it + is still legal but equivalent to intros ?a ?b. - New intro pattern "{A,B,C}" synonym to "(A,(B,C))" - New syntax "rewrite A,B" for "rewrite A; rewrite B" - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8dd168aad2..864a004fe1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1451,7 +1451,7 @@ An introduction pattern is either: \begin{itemize} \item the wildcard: {\tt \_} \item the pattern \texttt{?} -\item the pattern \texttt{@\ident} +\item the pattern \texttt{?\ident} \item a variable \item a disjunction of lists of patterns: {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]} @@ -1465,7 +1465,7 @@ structure of the pattern given as argument: immediately clear (cf~\ref{clear}) the corresponding hypothesis; \item introduction on \texttt{?} do the introduction, and let Coq choose a fresh name for the variable; -\item introduction on \texttt{@\ident} do the introduction, and let Coq +\item introduction on \texttt{?\ident} do the introduction, and let Coq choose a fresh name for the variable based on {\ident}; \item introduction on a variable behaves like described in~\ref{intro}; \item introduction over a diff --git a/interp/genarg.ml b/interp/genarg.ml index 2c61fc3c9b..930cfe7394 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -87,7 +87,7 @@ let rec pr_intro_pattern = function | IntroWildcard -> str "_" | IntroIdentifier id -> pr_id id | IntroAnonymous -> str "?" - | IntroFresh id -> str "@" ++ pr_id id + | IntroFresh id -> str "?" ++ pr_id id and pr_case_intro_pattern = function | [pl] -> diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9d0cd28ff0..7ec88618da 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -186,7 +186,7 @@ GEXTEND Gram | t::q -> IntroOrAndPattern [[t;pairify q]] in pairify tc | "_" -> IntroWildcard - | "@"; prefix = ident -> IntroFresh prefix + | "?"; prefix = ident -> IntroFresh prefix | "?" -> IntroAnonymous | id = ident -> IntroIdentifier id ] ] |