doc(Style): clarify indentation of documentation strings

templates/contribute/doc.md

@@ -88,6 +88,7 @@ Every definition and major theorem is required to have a doc string.
 or might be useful in another file.)
 These are introduced using `/--` and closed by `-/` above the definition, with either newlines or
 single spaces between the markers and the text.
+Subsequent lines in a doc-string should not be indented.
 They can contain Markdown and LaTeX as well: see the next section. If a doc string is a complete
 sentence, then it should end in a period. Named theorems, such as the **mean value theorem** should be bold faced (i.e., with
 two asterisks before and after).

templates/contribute/style.md

@@ -80,7 +80,8 @@ two main concepts in the theory of xyzzyology.
 ## Main results
 
 - `exists_foo`: the main existence theorem of `foo`s.
-- `bar_of_foo`: a construction of a `bar`, given a `foo`.
+- `bar_of_foo`: a construction of a `bar`, given a `foo` under very complicated
+  and intricate circumstances worth describing in excruciating detail.
 - `bar_eq`    : the main classification theorem of `bar`s.
 
 ## Notation
@@ -562,6 +563,8 @@ implementation notes) or for comments in proofs.
 Use `--` for short or in-line comments.
 
 Documentation strings for declarations are delimited with `/-- -/`.
+When a documentation string for a declaration spans multiple lines, do not indent
+subsequent lines.
 
 See our [documentation requirements](doc.html) for more suggestions
 and examples.