Better error messages
Ideas (from discussion with @snyke7):
-
Make it clearer what the top level connective is (maybe hide the continuation unless a certain flag is set or so) -
Have Ltac tactic that looks at goal to give a better error message: E.g. point out common mistakes -
Group Type and Prop hypothesis (maybe hide names of Prop hypothesis) -
Don't show dependent subgoals (i.e. not yet instantiated evars) -
Suggestions in #26 (comment 68542) -
LSP for RefinedC -
Display error messages -
Rollback proof and step it from the editor (probably would be hard to implement, but would be fancy)
-