diff --git a/src/Ledger/Address.lagda b/src/Ledger/Address.lagda
index db5b5e549..f5c46c8b9 100644
--- a/src/Ledger/Address.lagda
+++ b/src/Ledger/Address.lagda
@@ -14,6 +14,13 @@ We define credentials and various types of addresses here. A
 credential contains a hash, either of a verifying (public) key
 (\isVKey) or of a (\isScript).
 
+N.B.~in the Shelley era the type of the \stake field of the
+\BaseAddr record was \CredentialType; to specify an address with
+no stake, we would use an ``enterprise'' address. In contrast,
+the type of \stake in the Conway era is \Maybe~\CredentialType,
+so we can now use \BaseAddr to specify an address with no stake
+by setting \stake to \nothing.
+
 \begin{figure*}[h!]
 \begin{AgdaMultiCode}
 \emph{Abstract types}
diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty
index cbe4c524e..067aa940a 100644
--- a/src/latex/agda-latex-macros.sty
+++ b/src/latex/agda-latex-macros.sty
@@ -160,6 +160,8 @@
 \newcommand{\Anchor}{\AgdaRecord{Anchor}\xspace}
 \newcommand{\as}{\AgdaSymbol{as}\xspace}
 
+
+\newcommand{\BaseAddr}{\AgdaRecord{BaseAddr}\xspace}
 \newcommand{\beginstrict}{\AgdaFunction{begin-strict}\xspace}
 \newcommand{\Bool}{\AgdaDatatype{Bool}\xspace}
 
@@ -169,6 +171,7 @@
 \newcommand{\Coin}{\AgdaFunction{Coin}\xspace}
 \newcommand{\Computational}{\AgdaRecord{Computational}\xspace}
 \newcommand{\Credential}{\AgdaFunction{Credential}\xspace}
+\newcommand{\CredentialType}{\AgdaDatatype{Credential}\xspace}
 \newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace}
 \newcommand{\canVote}{\AgdaFunction{canVote}\xspace}
 \newcommand{\case}{\AgdaFunction{case}\xspace}
@@ -463,6 +466,7 @@
 \newcommand{\specProperty}{\AgdaFunction{specProperty}\xspace}
 \newcommand{\sprime}{\AgdaGeneralizable{s'}\xspace}
 \newcommand{\spring}{\AgdaFunction{sp-∘}\xspace}
+\newcommand{\stake}{\AgdaField{stake}\xspace}
 \newcommand{\stakeDistrs}{\AgdaField{stakeDistrs}\xspace}
 \newcommand{\stakeDistr}{\AgdaField{stakeDistr}\xspace}
 \newcommand{\subst}{\AgdaFunction{subst}\xspace}