removed section on documenting tactics, needs to be updated and restored

[kim-em]

I removed the following chunk from templates/contribute/doc.md. A replacement should eventually be restored...

## Tactic doc entries

Interactive tactics, user commands, hole commands and user attributes should have doc strings
explaining how they can be used. The `add_tactic_doc` command should be invoked afterwards to add a
doc entry to the appropriate page in the online docs.

Example:
```lean
/--
describe what the command does here
-/
add_tactic_doc
{ name := "display name of the tactic",
  category := cat,
  decl_names := [`dcl_1, `dcl_2],
  tags := ["tag_1", "tag_2"]
}

The argument to add_tactic_doc is a structure of type tactic_doc_entry.

• name refers to the display name of the tactic; it is used as the header of the doc entry.
• cat refers to the category of doc entry.
  Options: doc_category.tactic, doc_category.cmd, doc_category.hole_cmd, doc_category.attr
• decl_names is a list of the declarations associated with this doc. For instance,
  the entry for linarith would set decl_names := [`tactic.interactive.linarith].
  Some entries may cover multiple declarations.
  It is only necessary to list the interactive versions of tactics.
• tags is an optional list of strings used to categorize entries.
• The doc string is the body of the entry. It can be formatted with markdown.
  What you are reading now is taken from the description of add_tactic_doc.

If only one related declaration is listed in decl_names and if this
invocation of add_tactic_doc does not have a doc string, the doc string of
that declaration will become the body of the tactic doc entry. If there are
multiple declarations, you can select the one to be used by passing a name to
the inherit_description_from field.

If you prefer a tactic to have a doc string that is different then the doc entry, then between
the /-- -/ markers, write the desired doc string first, then --- surrounded by new lines,
and then the doc entry.

Note that providing a badly formed tactic_doc_entry to the command can result in strange error
messages.