From 7cf31f73600e5d7a88861ed76a3211a0772eabc8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Jul 2022 15:34:09 -0700 Subject: [PATCH] chore: update comment --- src/Lean/Elab/Do.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 7d7b476557..cad0617977 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1386,7 +1386,7 @@ mutual let body := doFor[3] withFreshMacroScope do /- Recall that `@` (explicit) disables `coeAtOutParam`. - We used `@` at `Stream` functions to make sure `coeAtOutParam` is not used. -/ + We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/ let toStreamApp ← withRef ys `(@toStream _ _ _ $ys) let auxDo ← `(do let mut s := $toStreamApp:term