Backporting 11445 from 8.2 to trunk (negative conditions in

SearchAbout + referring objects by their notation).



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

1 files changed, 87 insertions, 86 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 69f9b2f41..be5980fe4 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -142,94 +142,95 @@
 \newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
 
 
-\newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
-\newcommand{\Index}{\textrm{\textsl{index}}}
-\newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
-\newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
-\newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
-\newcommand{\cast}{\textrm{\textsl{cast}}}
-\newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
-\newcommand{\cofixpointbody}{\textrm{\textsl{cofix\_body}}}
-\newcommand{\commandtac}{\textrm{\textsl{tactic\_invocation}}}
-\newcommand{\constructor}{\textrm{\textsl{constructor}}}
-\newcommand{\convtactic}{\textrm{\textsl{conv\_tactic}}}
-\newcommand{\declarationkeyword}{\textrm{\textsl{declaration\_keyword}}}
-\newcommand{\declaration}{\textrm{\textsl{declaration}}}
-\newcommand{\definition}{\textrm{\textsl{definition}}}
-\newcommand{\digit}{\textrm{\textsl{digit}}}
-\newcommand{\exteqn}{\textrm{\textsl{ext\_eqn}}}
-\newcommand{\field}{\textrm{\textsl{field}}}
-\newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}
-\newcommand{\fixpg}{\textrm{\textsl{fix\_pgm}}}
-\newcommand{\fixpointbodies}{\textrm{\textsl{fix\_bodies}}}
-\newcommand{\fixpointbody}{\textrm{\textsl{fix\_body}}}
-\newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
-\newcommand{\flag}{\textrm{\textsl{flag}}}
-\newcommand{\form}{\textrm{\textsl{form}}}
-\newcommand{\entry}{\textrm{\textsl{entry}}} 
-\newcommand{\proditem}{\textrm{\textsl{production\_item}}} 
-\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}}
-\newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} 
-\newcommand{\scope}{\textrm{\textsl{scope}}} 
-\newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} 
-\newcommand{\declnotation}{\textrm{\textsl{decl\_notation}}} 
-\newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
-\newcommand{\modifiers}{\textrm{\textsl{modifiers}}}
-\newcommand{\localdef}{\textrm{\textsl{local\_def}}}
-\newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}
-\newcommand{\ident}{\textrm{\textsl{ident}}}
-\newcommand{\accessident}{\textrm{\textsl{access\_ident}}}
-\newcommand{\possiblybracketedident}{\textrm{\textsl{possibly\_bracketed\_ident}}}
-\newcommand{\inductivebody}{\textrm{\textsl{ind\_body}}}
-\newcommand{\inductive}{\textrm{\textsl{inductive}}}
-\newcommand{\naturalnumber}{\textrm{\textsl{natural}}}
-\newcommand{\integer}{\textrm{\textsl{integer}}}
-\newcommand{\multpattern}{\textrm{\textsl{mult\_pattern}}}
-\newcommand{\mutualcoinductive}{\textrm{\textsl{mutual\_coinductive}}}
-\newcommand{\mutualinductive}{\textrm{\textsl{mutual\_inductive}}}
-\newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
-\newcommand{\name}{\textrm{\textsl{name}}}
-\newcommand{\num}{\textrm{\textsl{num}}}
-\newcommand{\pattern}{\textrm{\textsl{pattern}}}
-\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
-\newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
-\newcommand{\disjconjintropattern}{\textrm{\textsl{disj\_conj\_intro\_pattern}}}
-\newcommand{\namingintropattern}{\textrm{\textsl{naming\_intro\_pattern}}}
-\newcommand{\pat}{\textrm{\textsl{pat}}}
-\newcommand{\pgs}{\textrm{\textsl{pgms}}}
-\newcommand{\pg}{\textrm{\textsl{pgm}}}
+\newcommand{\Fwterm}{\nterm{Fwterm}}
+\newcommand{\Index}{\nterm{index}}
+\newcommand{\abbrev}{\nterm{abbreviation}}
+\newcommand{\atomictac}{\nterm{atomic\_tactic}}
+\newcommand{\bindinglist}{\nterm{bindings\_list}}
+\newcommand{\cast}{\nterm{cast}}
+\newcommand{\cofixpointbodies}{\nterm{cofix\_bodies}}
+\newcommand{\cofixpointbody}{\nterm{cofix\_body}}
+\newcommand{\commandtac}{\nterm{tactic\_invocation}}
+\newcommand{\constructor}{\nterm{constructor}}
+\newcommand{\convtactic}{\nterm{conv\_tactic}}
+\newcommand{\declarationkeyword}{\nterm{declaration\_keyword}}
+\newcommand{\declaration}{\nterm{declaration}}
+\newcommand{\definition}{\nterm{definition}}
+\newcommand{\digit}{\nterm{digit}}
+\newcommand{\exteqn}{\nterm{ext\_eqn}}
+\newcommand{\field}{\nterm{field}}
+\newcommand{\firstletter}{\nterm{first\_letter}}
+\newcommand{\fixpg}{\nterm{fix\_pgm}}
+\newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
+\newcommand{\fixpointbody}{\nterm{fix\_body}}
+\newcommand{\fixpoint}{\nterm{fixpoint}}
+\newcommand{\flag}{\nterm{flag}}
+\newcommand{\form}{\nterm{form}}
+\newcommand{\entry}{\nterm{entry}} 
+\newcommand{\proditem}{\nterm{production\_item}} 
+\newcommand{\taclevel}{\nterm{tactic\_level}}
+\newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
+\newcommand{\scope}{\nterm{scope}} 
+\newcommand{\delimkey}{\nterm{key}} 
+\newcommand{\optscope}{\nterm{opt\_scope}} 
+\newcommand{\declnotation}{\nterm{decl\_notation}} 
+\newcommand{\symbolentry}{\nterm{symbol}}
+\newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\localdef}{\nterm{local\_def}}
+\newcommand{\localdecls}{\nterm{local\_decls}}
+\newcommand{\ident}{\nterm{ident}}
+\newcommand{\accessident}{\nterm{access\_ident}}
+\newcommand{\possiblybracketedident}{\nterm{possibly\_bracketed\_ident}}
+\newcommand{\inductivebody}{\nterm{ind\_body}}
+\newcommand{\inductive}{\nterm{inductive}}
+\newcommand{\naturalnumber}{\nterm{natural}}
+\newcommand{\integer}{\nterm{integer}}
+\newcommand{\multpattern}{\nterm{mult\_pattern}}
+\newcommand{\mutualcoinductive}{\nterm{mutual\_coinductive}}
+\newcommand{\mutualinductive}{\nterm{mutual\_inductive}}
+\newcommand{\nestedpattern}{\nterm{nested\_pattern}}
+\newcommand{\name}{\nterm{name}}
+\newcommand{\num}{\nterm{num}}
+\newcommand{\pattern}{\nterm{pattern}}
+\newcommand{\orpattern}{\nterm{or\_pattern}}
+\newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
+\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
+\newcommand{\pat}{\nterm{pat}}
+\newcommand{\pgs}{\nterm{pgms}}
+\newcommand{\pg}{\nterm{pgm}}
 %BEGIN LATEX
-\newcommand{\proof}{\textrm{\textsl{proof}}}
+\newcommand{\proof}{\nterm{proof}}
 %END LATEX
-%HEVEA \renewcommand{\proof}{\textrm{\textsl{proof}}}
-\newcommand{\record}{\textrm{\textsl{record}}}
-\newcommand{\rewrule}{\textrm{\textsl{rewriting\_rule}}}
-\newcommand{\sentence}{\textrm{\textsl{sentence}}}
-\newcommand{\simplepattern}{\textrm{\textsl{simple\_pattern}}}
-\newcommand{\sort}{\textrm{\textsl{sort}}}
-\newcommand{\specif}{\textrm{\textsl{specif}}}
-\newcommand{\statement}{\textrm{\textsl{statement}}}
-\newcommand{\str}{\textrm{\textsl{string}}}
-\newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
-\newcommand{\switch}{\textrm{\textsl{switch}}}
-\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
-\newcommand{\tac}{\textrm{\textsl{tactic}}}
-\newcommand{\terms}{\textrm{\textsl{terms}}}
-\newcommand{\term}{\textrm{\textsl{term}}}
-\newcommand{\module}{\textrm{\textsl{module}}}
-\newcommand{\modexpr}{\textrm{\textsl{module\_expression}}}
-\newcommand{\modtype}{\textrm{\textsl{module\_type}}}
-\newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
-\newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
-\newcommand{\qualid}{\textrm{\textsl{qualid}}}
-\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}}
-\newcommand{\class}{\textrm{\textsl{class}}}
-\newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
-\newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}}
-\newcommand{\type}{\textrm{\textsl{type}}}
-\newcommand{\vref}{\textrm{\textsl{ref}}}
-\newcommand{\zarithformula}{\textrm{\textsl{zarith\_formula}}}
-\newcommand{\zarith}{\textrm{\textsl{zarith}}}
+%HEVEA \renewcommand{\proof}{\nterm{proof}}
+\newcommand{\record}{\nterm{record}}
+\newcommand{\rewrule}{\nterm{rewriting\_rule}}
+\newcommand{\sentence}{\nterm{sentence}}
+\newcommand{\simplepattern}{\nterm{simple\_pattern}}
+\newcommand{\sort}{\nterm{sort}}
+\newcommand{\specif}{\nterm{specif}}
+\newcommand{\statement}{\nterm{statement}}
+\newcommand{\str}{\nterm{string}}
+\newcommand{\subsequentletter}{\nterm{subsequent\_letter}}
+\newcommand{\switch}{\nterm{switch}}
+\newcommand{\messagetoken}{\nterm{message\_token}}
+\newcommand{\tac}{\nterm{tactic}}
+\newcommand{\terms}{\nterm{terms}}
+\newcommand{\term}{\nterm{term}}
+\newcommand{\module}{\nterm{module}}
+\newcommand{\modexpr}{\nterm{module\_expression}}
+\newcommand{\modtype}{\nterm{module\_type}}
+\newcommand{\onemodbinding}{\nterm{module\_binding}}
+\newcommand{\modbindings}{\nterm{module\_bindings}}
+\newcommand{\qualid}{\nterm{qualid}}
+\newcommand{\qualidorstring}{\nterm{qualid\_or\_string}}
+\newcommand{\class}{\nterm{class}}
+\newcommand{\dirpath}{\nterm{dirpath}}
+\newcommand{\typedidents}{\nterm{typed\_idents}}
+\newcommand{\type}{\nterm{type}}
+\newcommand{\vref}{\nterm{ref}}
+\newcommand{\zarithformula}{\nterm{zarith\_formula}}
+\newcommand{\zarith}{\nterm{zarith}}
 \newcommand{\ltac}{\mbox{${\cal L}_{tac}$}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%