doc(data/quot): promote a comment to a docstring (#7306)

leanprover-community · Apr 21, 2021 · f08fe5f · f08fe5f
1 parent 7db1181
commit f08fe5f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/data/quot.lean b/src/data/quot.lean
@@ -335,9 +335,9 @@ namespace quotient
 variables {γ : Sort*} {φ : Sort*}
   {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ}
 
-/- Versions of quotient definitions and lemmas ending in `'` use unification instead
+/-! Versions of quotient definitions and lemmas ending in `'` use unification instead
 of typeclass inference for inferring the `setoid` argument. This is useful when there are
-several different quotient relations on a type, for example quotient groups, rings and modules -/
+several different quotient relations on a type, for example quotient groups, rings and modules. -/
 
 /-- A version of `quotient.mk` taking `{s : setoid α}` as an implicit argument instead of an
 instance argument. -/