Don't advance if Coq reports an error.
Add indentation and comment rules.
Remove stale Basics.v.
Add completions.