aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-01-29 15:34:15 +0100
committerGaëtan Gilbert2019-01-29 15:35:05 +0100
commitde9a5897eb2b7d325f7f65a5c30f71203be05834 (patch)
treec9e66c34b7ce7acd95eea35abfe62bfb1ec8dc19
parenta9b141469fe3036355be95d8cf5f0bf5c240fe37 (diff)
Use \mathcal instead of \cal
Apparently it's deprecated / doesn't always work, see https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m See #9429 (we also need to fix the distributed file on the server).
-rw-r--r--dev/doc/versions-history.tex2
-rw-r--r--doc/common/macros.tex10
-rw-r--r--doc/sphinx/refman-preamble.sty8
3 files changed, 10 insertions, 10 deletions
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 8f9c3171da..1c4913d201 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \
& & \feature{kernel-centric} architecture \\
& & more care for outside readers\\
& & (indentation, ocaml warning protection)\\
-Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\
+Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\
Coq V7.0beta2& released 2 February 2001\\
Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6a28c5b3d1..927a912fbf 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -242,7 +242,7 @@
\newcommand{\vref}{\nterm{ref}}
\newcommand{\zarithformula}{\nterm{zarith\_formula}}
\newcommand{\zarith}{\nterm{zarith}}
-\newcommand{\ltac}{\mbox{${\cal L}_{tac}$}}
+\newcommand{\ltac}{\mbox{${\mathcal{L}}_{tac}$}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \mbox{\sf } series for roman text in maths formulas %
@@ -373,15 +373,15 @@
\newcommand{\sumbool}[2]{\{#1\}+\{#2\}}
\newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
\newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
-\newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
-\newcommand{\WFTWOLINES}[2]{\ensuremath{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}}
+\newcommand{\WF}[2]{\ensuremath{{\mathcal{W\!F}}(#1)[#2]}}
+\newcommand{\WFTWOLINES}[2]{\ensuremath{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
-\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}}
+\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\mathcal{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$}}
@@ -427,7 +427,7 @@
\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
\newcommand{\subst}[3]{#1\{#2/#3\}}
\newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}}
-\newcommand{\Sort}{\mbox{$\cal S$}}
+\newcommand{\Sort}{\mbox{$\mathcal{S}$}}
\newcommand{\convert}{=_{\beta\delta\iota\zeta\eta}}
\newcommand{\leconvert}{\leq_{\beta\delta\iota\zeta\eta}}
\newcommand{\NN}{\mathbb{N}}
diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty
index cb7c8d0cf5..8f7b1bb1e8 100644
--- a/doc/sphinx/refman-preamble.sty
+++ b/doc/sphinx/refman-preamble.sty
@@ -63,7 +63,7 @@
\newcommand{\Set}{\textsf{Set}}
\newcommand{\si}{\textsf{if}}
\newcommand{\sinon}{\textsf{else}}
-\newcommand{\Sort}{\cal S}
+\newcommand{\Sort}{\mathcal{S}}
\newcommand{\Str}{\textsf{Stream}}
\newcommand{\Struct}{\kw{Struct}}
\newcommand{\subst}[3]{#1\{#2/#3\}}
@@ -75,10 +75,10 @@
\newcommand{\unfold}{\textsf{unfold}}
\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}}
\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
-\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
+\newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]}
\newcommand{\WFE}[1]{\WF{E}{#1}}
-\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
-\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
+\newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)}
+\newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
\newcommand{\with}{\kw{with}}
\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}