New command Declare Reduction <id> := <conv_expr>.

 Let's avoid writing huge "Eval ... in ..." lines :-)
 Will be used in particular soon in NMake for defining function via
  Definition ... := Eval ... in ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 316a02f1b..c71df4e22 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1020,6 +1020,21 @@ command is prefixed by {\tt Local}. In the latter case, the behavior
 regarding sections and modules is the same as for the {\tt
   Transparent} and {\tt Opaque} commands.
 
+\subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.}
+
+This command allows to give a short name to a reduction expression,
+for instance {\tt lazy beta delta [foo bar]}. This short name can
+then be used in {\tt Eval \ident\ in ...} or {\tt eval} directives.
+This command accepts the {\tt Local} modifier, for discarding
+this reduction name at the end of the file or module. For the moment
+the name cannot be qualified. In particular declaring the same name
+in several modules or in several functor applications will be refused
+if these declarations are not local. The name \ident\ cannot be used
+directly as an Ltac tactic, but nothing prevent the user to also
+perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}.
+
+\SeeAlso sections \ref{Conversion-tactics}
+
 \subsection{\tt Set Virtual Machine
 \label{SetVirtualMachine}
 \comindex{Set Virtual Machine}}