diff options
author | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 07:40:43 +0000 |
---|---|---|
committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 07:40:43 +0000 |
commit | 1c38e7101eb54594b06111271369cbffac50c3b6 (patch) | |
tree | 5ff88aa5ea73d48b9d6d65754212ee042b59b435 /doc/common/macros.tex | |
parent | c82f88f9dd833dc33dacfe03822bc5987041e6ac (diff) |
Correction bug 1838 + doc modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10821 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/common/macros.tex')
-rwxr-xr-x | doc/common/macros.tex | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 3bfe09c16..47baa94a6 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -270,7 +270,6 @@ \newcommand{\T}{\texttt{T}} \newcommand{\U}{\texttt{U}} \newcommand{\real}{\textsf{Real}} -\newcommand{\Spec}{\textit{Spec}} \newcommand{\Data}{\textit{Data}} \newcommand{\In} {{\textbf{in }}} \newcommand{\AND} {{\textbf{and}}} @@ -356,6 +355,8 @@ \newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}} \newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}} \newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}} @@ -404,14 +405,25 @@ \newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}} \newcommand{\Impl}{{\it Impl}} +\newcommand{\elem}{{\it e}} \newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})} +\newcommand{\ModS}[2]{{\sf Mod}({#1}:{#2})} \newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})} -\newcommand{\ModS}[2]{{\sf ModS}({#1}:{#2})} -\newcommand{\ModSEq}[3]{{\sf ModSEq}({#1}:{#2}=={#3})} +\newcommand{\ModA}[2]{{\sf ModA}({#1}=={#2})} \newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}} \newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}} \newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}} \newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}} +\newcommand{\structe}[1]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2};\ldots + ;\elem_n~{\sf End}}} +\newcommand{\structes}[2]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2}\{#2\} + ;\ldots;\elem_n\{#2\}~{\sf End}}} +\newcommand{\with}[3]{\ensuremath{#1~{\sf with}~#2 := #3}} + +\newcommand{\Spec}{{\it Spec}} +\newcommand{\ModSEq}[3]{{\sf Mod}({#1}:{#2}:={#3})} %\newbox\tempa |