Full-autocomplete for teachers #177
Description
Currently, teachers have access to the same autocomplete as students. This makes it tedious to write some proofs.
In particular, arguments to "Assume that" and "Take" could be inferred.
Because the autocompletion is mostly in the frontend, but this requires data from coq-waterproof, this feature needs an interplay between the two components.
We need a switch to turn this on, because we don't want students to use this. It probably needs an option in coq-waterproof, possibly along with an activated teacher mode in waterproof-vscode.
Acceptance criteria:
- A proper switch for this feature is implemented
- If this switch is turned on, Assume that is autocompleted with the antecedent, if the goal is an implication.
- If this switch is turned on, Take is autocompleted with the correct parameters if the goal is a for all.