feat(tactic/linarith): better input syntax linarith only [...] (#1056)
* feat(tactic/ring, tactic/linarith): add reducibility parameter
* fix(tactic/ring): interactive parsing for argument to ring1
* feat(tactic/linarith): better input syntax linarith only [...]
* fix(docs/tactics): fix linarith doc