Pierre Courtieu
Pierre Courtieu
Maybe I need to test how it interacts with debug mode. I don't have much time this week though.
@hendriktews can you tell us what remains to be tested/adapted pls? I think this PR should not rot. You said elsewhere that the prefix arg C-u for queries like coq-Print...
> I use this code on a daily basis, so it is working for me. Remaining things that I know: > > * coq-Print with prefix arg > > *...
> > > * Not sure if this is a problem: [...] This might make the impression, search does not work at all. > > > > > > I...
The change is nice. A few remarks here and there. 2 questions: - should we remove the code that displays this information in the scritpting buffer then? - the `coq-test-coqtop-unavailable.el`...
The PR should first be cleaned up (useless files, then reduced to one commit imho.
My opinion is that everything should be customizable, but I don't always apply it to myself. I think the current goal counter (on the scripting buffer) is not customizable either.
I have been thinking about this PR a bit more and I think we should not merge it. 1. This feature (having the number of goals in the modeline) already...
Hi. Sadly the `coq-smie-user-tokens` variable that usually can solve this kind of problem does not work in this case because "\\" is not considered as part f a token by...
Actually I think I found a simple way to fix this. @KimayaBedarkar can you test this? I get this indentation now: ```coq Require Import mathcomp.ssreflect.ssrbool. Definition xx := nat. Module...