diff options
author | 2008-05-11 22:04:26 +0000 | |
---|---|---|
committer | 2008-05-11 22:04:26 +0000 | |
commit | 30443ddaba7a0cc996216b3d692b97e0b05907fe (patch) | |
tree | 1a1bdadcdf69582262bd6bddc21e9e03215d2871 /doc/refman/RefMan-ltac.tex | |
parent | b6c6e36afa8da16a62bf16191baa2531894c54fc (diff) |
- Cleanup parsing of binders, reducing to a single production for all
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d9a1d4756..fc5f4e4cb 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -187,7 +187,9 @@ is understood as \begin{tabular}{lcl} \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\ \\ -\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr} +\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} +{\tacexpr}\\ +& $|$ &{\qualid} \sequence{\ident}{} {\tt ::=}{\tacexpr} \end{tabular} \end{centerframe} \caption{Tactic toplevel definitions} @@ -831,11 +833,15 @@ possible with the syntax: {\tacexpr}$_n$ \end{quote} -%This definition bloc is a set of definitions (use of -%the same previous syntactical sugar) and the other scripts are evaluated as -%usual except that the substitutions are lazily carried out (when an identifier -%to be evaluated is the name of a recursive definition). - +It is also possible to \emph{redefine} an existing user-defined tactic +using the syntax: +\begin{quote} +{\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=} +{\tacexpr} +\end{quote} +A previous definition of \qualid must exist in the environment. +The new definition will always be used instead of the old one and +it goes accross module boundaries. \subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}} |