Enforce uniform indentation in tactic blocks / do blocks / sepByIndent

[gebner]

The use of colGe to implement indentation-sensitive syntax can lead to extremely surprising parses:

example : false := by
  conv =>
    lhs
    dsimp
    simp

Namely if dsimp is a conv-tactic then this parses as three conv-tactics (like the indentation suggests). But if dsimp is not a conv-tactic, then this parses as (conv => lhs); dsimp; simp.

We should try out whether a colEq combinator (that enforces uniform indentation) causes any unexpected issues.

Another option (that fixes the particular issue here) would be to implement a fallback elab ident : conv => throwError "unknown conv tactic" like we have for tactic.

[leodemoura]

We should try out whether a colEq combinator (that enforces uniform indentation) causes any unexpected issues.

I like this.