diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -3,6 +3,8 @@
 OTT_OPTS  = -tex_show_meta false
 TARGET    = core-spec
 
+all: $(TARGET).pdf
+
 $(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
 	latex -output-format=pdf $<
 	latex -output-format=pdf $<
@@ -13,6 +15,6 @@
 $(OTT_TEX): $(OTT_FILES)
 	ott -tex_wrap false $(OTT_OPTS) -o $@ $^
 
-.PHONY: clean
+.PHONY: all clean
 clean:
 	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log *.fls
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -188,14 +188,18 @@
 a term-level literal, but we are ignoring this distinction here.
 \item A coercion used as a type should appear only in the right-hand side of
   an application.
+\item If $[[forall n. t]]$ is a polymorphic type over a coercion variable (i.e.
+  $[[n]]$ is a coercion variable), then $[[n]]$ must appear in $[[t]]$;
+  otherwise it should be represented as a \texttt{FunTy}. See \texttt{Note
+    [Unused coercion variable in ForAllTy]} in \ghcfile{types/TyCoRep.hs}.
 \end{itemize}
 
 Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
 are purely representational. The metatheory would remain the same if these forms
 were removed in favor of $[[t1 t2]]$. Nevertheless, we keep all three forms in
 this documentation to accurately reflect the implementation.
 
-The \texttt{ArgFlag} field of a \texttt{TyVarBinder} (the first argument to a
+The \texttt{ArgFlag} field of a \texttt{TyCoVarBinder} (the first argument to a
 \texttt{ForAllTy}) also tracks visibility of arguments. Visibility affects
 only source Haskell, and is omitted from this presentation.
 
@@ -216,6 +220,10 @@
 \item The name in a coercion must be a term-level name (\ctor{Id}).
 \item The contents of $[[<t>]]$ must not be a coercion. In other words,
 the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
+\item If $[[forall z: h .g]]$ is a polymorphic coercion over a coercion variable
+  (i.e. $[[z]]$ is a coercion variable), then $[[z]]$ can only appear in
+  \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note[Unused coercion
+    variable in ForAllCo] in \ghcfile{types/Coercion.hs}}.
 \end{itemize}
 
 The \texttt{UnivCo} constructor takes several arguments: the two types coerced
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 0000000000000000000000000000000000000000..0000000000000000000000000000000000000000
GIT binary patch
literal 0
Hc$@<O00001

literal 0
Hc$@<O00001