diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-11 18:35:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-11 18:35:31 +0000 |
commit | 76dfe2df5a5fc4623384a04610ba9f73030fee60 (patch) | |
tree | fd2dca003e37beb1d4cfa6d21f655ccc0edbd8b5 /doc/common/macros.tex | |
parent | 2e6c3a7b0b12cfd3b560de60f4918063f149fd01 (diff) |
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
Diffstat (limited to 'doc/common/macros.tex')
-rwxr-xr-x | doc/common/macros.tex | 173 |
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}$}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |