Commit 2020-09-03 00:15 7b9db99c

fix(test/*): make sure tests produce no output (#3947) Modify tests so that they produce no output. This also means removing all uses of sorry/admit. Replace #eval by run_cmd consistently. Tests that produced output before are modified so that it is checked that they roughly produce the right output Add a trace option to the #simp command that turns the message of only if the expression is simplified to true. All tests are modified so that they simplify to true. The randomized tests can produce output when they find a false positive, but that should basically never happen. Add some docstings to src/tactic/interactive.