From bb499fdd7a35bd9df1fbd323c9a84d31f063851f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 2 Feb 2016 09:17:48 +0100
Subject: [PATCH] make sure macros do not leak across files
---
_CoqProject | 2 +-
docs/iris.tex | 14 +++++++-------
docs/logic.tex | 9 ++++-----
docs/model.tex | 4 ++--
docs/setup.tex | 2 ++
5 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 3eaad9889..e51a099d6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,4 @@
--Q . ""
+s-Q . ""
prelude/option.v
prelude/fin_map_dom.v
prelude/bsets.v
diff --git a/docs/iris.tex b/docs/iris.tex
index 3a4b55697..b0bd1b4bb 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -38,17 +38,17 @@
%\clearpage
\tableofcontents
-\clearpage
+\clearpage\begingroup
\input{algebra}
-\clearpage
+\endgroup\clearpage\begingroup
\input{constructions}
-\clearpage
+\endgroup\clearpage\begingroup
\input{logic}
-\clearpage
+\endgroup\clearpage\begingroup
\input{model}
-\clearpage
+\endgroup\clearpage\begingroup
\input{derived}
-
-\clearpage\printbibliography % If we want biblatex
+\endgroup\clearpage\begingroup
+\printbibliography
\end{document}
diff --git a/docs/logic.tex b/docs/logic.tex
index 02f684de6..e991d07a8 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -106,13 +106,12 @@ to express that $\sigfn$ is a function symbol with the indicated arity.
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
-\newcommand{\unitterm}{()}%
-\newcommand{\unitsort}{1}% \unit is bold.
+
\begin{align*}
\term, \prop, \pred ::={}&
x \mid
\sigfn(\term_1, \dots, \term_n) \mid
- \unitterm \mid
+ \unitval \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam x.\term \mid
@@ -174,7 +173,7 @@ We introduce additional metavariables ranging over terms and generally let the c
\]
\paragraph{Variable conventions.}
-We often abuse notation, using the preceding \emph{term} metavariables to range over (bound) \emph{variables}.
+We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
We omit type annotations in binders, when the type is clear from context.
@@ -211,7 +210,7 @@ In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $
}
%%% products
\and
- \axiom{\vctx \proves \wtt{\unitterm}{\unitsort}}
+ \axiom{\vctx \proves \wtt{\unitval}{\unitsort}}
\and
\infer{\vctx \proves \wtt{\term}{\sort_1} \and \vctx \proves \wtt{\termB}{\sort_2}}
{\vctx \proves \wtt{(\term,\termB)}{\sort_1 \times \sort_2}}
diff --git a/docs/model.tex b/docs/model.tex
index 10c513cbd..c3d8fd168 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -11,7 +11,7 @@ an equivalence relation over $X$ satisfying
\item $\All x,x',n. x \nequiv{n+1} x' \implies x \nequiv{n} x',$
\item $\All x,x'. (\All n. x\nequiv{n} x') \implies x = x'.$
\end{itemize}
-
+\a
Let $(X,(\nequivset{n}{X})_{n\in\mathbb{N}})$ and
$(Y,(\nequivset{n}{Y})_{n\in\mathbb{N}})$ be o.f.e.'s. A function $f:
X\to Y$ is \emph{non-expansive} if, for all $x$, $x'$ and $n$,
@@ -431,7 +431,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\Lam v : \Sem{\sort}. \Sem{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\
\Sem{\vctx \proves \term~\termB : \sort'}_\gamma &=
\Sem{\vctx \proves \term : \sort \to \sort'}_\gamma(\Sem{\vctx \proves \termB : \sort}_\gamma) \\
- \Sem{\vctx \proves \unitterm : \unitsort}_\gamma &= \star \\
+ \Sem{\vctx \proves \unitval : \unitsort}_\gamma &= \star \\
\Sem{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\Sem{\vctx \proves \term_1 : \sort_1}_\gamma, \Sem{\vctx \proves \term_2 : \sort_2}_\gamma) \\
\Sem{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\Sem{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma)
\end{align*}
diff --git a/docs/setup.tex b/docs/setup.tex
index 0e2f64722..e16fbecf9 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -307,6 +307,8 @@
\newcommand{\mask}{\mathcal{E}}
%% various pieces of Syntax
+\newcommand{\unitsort}{1}% \unit is bold.
+
\def\MU #1.{\mu #1.\;}%
\def\Lam #1.{\lambda #1.\;}%
--
GitLab