From 1c692d39ea1a19a8644a3f0be0b89c5a04705fdf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Aug 2016 10:49:17 +0200
Subject: [PATCH] Fix use of undefined universe "U"
Fixes #28
---
docs/model.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/docs/model.tex b/docs/model.tex
index 166b3ef6e..4b68fda07 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -152,7 +152,7 @@ The remaining domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
-For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\cal U$ and define
+For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
\[
\Sem{\type} \eqdef X_\type
\]
--
GitLab