From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 11 May 2008 22:04:26 +0000
Subject: - 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
---
 doc/refman/RefMan-ltac.tex | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d9a1d47563..fc5f4e4cb6 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}}
 
-- 
cgit v1.2.3