arend-lib
arend-lib copied to clipboard
Not intuitive error message of mcases tactic.
If the user forgets to surround mcases tactic with parentheses he won't get an error message. Instead he will get "missing clauses" message (despite the fact that clauses are present and no syntactic error is reported!)