Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

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}

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}}

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*}

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.\;}%