aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman')
-rw-r--r--doc/refman/RefMan-gal.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 64afc1aed4..f7a631d9ca 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -913,6 +913,8 @@ section and depending on {\ident} are prefixed by the let-in definition
\begin{Variants}
\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.}
+\item {\tt Let Fixpoint {\ident} \nelist{\fixpointbody}{with} {\tt .}.}
+\item {\tt Let CoFixpoint {\ident} \nelist{\cofixpointbody}{with} {\tt .}.}
\end{Variants}
\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},