From 64e7f25ffe81c4d8b7d79ea4e8adf689d9cc0317 Mon Sep 17 00:00:00 2001
From: Ed Ayers <EdAyers@users.noreply.github.com>
Date: Tue, 27 Sep 2022 13:48:29 +0100
Subject: [PATCH] doc: apply suggestions from code review

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
---
 src/Lean/Message.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index a6f5676402..1f3eb81077 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -37,7 +37,7 @@ structure NamingContext where
   currNamespace : Name
   openDecls : List OpenDecl
 
-/-- Structure message data. We use it for reporting errors, trace messages, etc. -/
+/-- Structured message data. We use it for reporting errors, trace messages, etc. -/
 inductive MessageData where
   | ofFormat          : Format → MessageData
   | ofSyntax          : Syntax → MessageData