From 7686f7b3e37b820bdc483b90247ddb53ab21776c Mon Sep 17 00:00:00 2001 From: ia0 Date: Tue, 14 Jul 2026 11:44:31 +0200 Subject: [PATCH] doc: add blank line after list in omega docstring This PR fixes the formatting of the `omega` tactic docstring so the concluding text renders as a separate paragraph rather than as part of the last list item. --- src/Init/Tactics.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 1bafb4df5692..4b6686d92b55 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1523,6 +1523,7 @@ can be used to: * `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary. * `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary. * `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b` + Currently, all of these are on by default. -/ syntax (name := omega) "omega" optConfig : tactic