Pierre Courtieu
Pierre Courtieu
From the number of issues raised by the diff mode for company-coq I suspect it relies too much on the `*coq*` content and should maybe migrate to looking more into...
Right, relying on this variable seems better. Maybe we could try to clean that variable from the tags in PG instead. Would it make other features fail? Otherwise we just...
Yes probably. Hopefully we don't get into efficiency problems.
For instance after the keyword "in" we should propose immediately hypothesis names.
This is an old subject. Inversion as clause has a bad semantic imho. It is used by inversion to give names to intermediate hypothesis instead of *final* hypothesis. So for...
The current experiment I am making on a private coq branch (https://github.com/Matafou/coq/tree/v8.5-compactcontexts, use "Set Compact Context") uses the following heuristic: if a sequence of hypothesis has sort Type, then print...
To answer Clément's question, it is probably not so difficult to have a decent diff mode while in compact mode: 1) difference in the compact part are probably not very...
Notice that ediff-buffer allows for this kind of things. P. 2016-01-26 7:06 GMT+01:00 Clément Pit--Claudel [email protected]: > Some preliminary thoughts, however: > - With just GNU diff, it seems tricky;...
In some interactive diff mode in emacs we can focus one diff to see the difference at the word level. Isn'it what you are looking for? P Le mar. 26...
Sounds good. But PG is really not made to be used by the emacs session that has compiled it. Does compilation fail? Or is it just when loading a prover...