From 5ae4b17ab09b81ba133f13e383106a4f9620d5d4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 28 Jan 2010 17:27:46 +0000 Subject: New command Declare Reduction := . 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 --- doc/refman/RefMan-oth.tex | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'doc') diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 316a02f1bd..c71df4e224 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}} -- cgit v1.2.3