Removing holes #862
Merged
Removing holes #862
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
coq-show (C-c C-a C-s) used to be smart and tried to look at the cursor position. If the cursos was on the locked region it tried to extract the goal state as stored at this point. But states are not stored anymore (coq runs silently now). This was marked as disabled in comments but the code was not unplugged. Even if this becomes possible again I think this feature (looking at the goal at point in file instead of at the end of locked region) needs to be a different command.
Move the declaration of user options coq-use-yasnippet and coq-yasnippet-use-default-templates to remove a cyclic dependency. Insertion of named goals is OK. But scripting does not support the use of curly braces together with them (which is there main advantage imho). This will be fixed in another PR.
Contributor
Author
|
@strub @dominique-unruh do you confirm you don't use holes.el. |
Contributor
|
I don't use holes.el. |
Contributor
|
Pinging @MM45 |
|
Good to go for me, EasyCrypt extension doesn't use |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Holes is a poor man's yasnippet that I wrote a long time ago. Yasnippet is 1) much better 2) maintained by someone else. Hence I am happy to remove this library from proofgeneral. The policy is: if if yasnippet is present then we use it by default (unless company-coq is present and takes precedence). Otherwise a very basic abbreviation system is used. One can opt out from yasnippet with
coq-use-yasnippetand independently one can opt out from the default yasnippet templates we build from coq-db.I will merge once maintainers pf other proof assistant instances confirm they don't need it.