diff --git a/source/declarations.tex b/source/declarations.tex
index b872574a39..7fcee1a752 100644
--- a/source/declarations.tex
+++ b/source/declarations.tex
@@ -8316,6 +8316,9 @@
 The attribute may be applied to the function type of a function declaration.
 A postcondition may introduce an identifier to represent
 the glvalue result or the prvalue result object of the function.
+When the declared return type of a non-templated function
+contains a placeholder type,
+the optional \grammarterm{identifier} shall only be present in a definition.
 \begin{example}
 \begin{codeblock}
 int f(char * c)
@@ -8323,6 +8326,9 @@
 
 int g(double * p)
   [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];
+
+auto h(int x)
+  [[ensures res: true]];       // error: cannot name the return value
 \end{codeblock}
 \end{example}
 
@@ -8436,7 +8442,10 @@
 \pnum
 The predicate of a contract condition has the same semantic restrictions
 as if it appeared as the first \grammarterm{expression-statement}
-in the body of the function it applies to.
+in the body of the function it applies to,
+except that the return type of the function is
+known in a contract condition appertaining to its definition,
+even if the return type contains a placeholder type.
 
 \pnum
 A precondition is checked by evaluating its predicate
diff --git a/source/templates.tex b/source/templates.tex
index 80584fce67..1af8343a13 100644
--- a/source/templates.tex
+++ b/source/templates.tex
@@ -5085,6 +5085,11 @@
 \mname{func}\iref{dcl.fct.def.general}, where any enclosing function is a
 template, a member of a class template, or a generic lambda,
 
+\item
+the \grammarterm{identifier} introduced in
+a postcondition\iref{dcl.attr.contract} to represent the result of
+a templated function whose declared return type contains a placeholder type,
+
 \item
 a
 \grammarterm{template-id}