Pierre Courtieu
Pierre Courtieu
@thirs can you describe the procedure to obtain this error? Is it when installing the elpa package?
> Weird: proof-general is there twice, once as installed, once as obsolete, with the same version. But installation failed so I guess this is more a consequence of the failure...
I tried this and I do not see any problem. ``` $ git clone https://github.com/melpa/melpa $ cd melpa $ make clean-packages clean-sandbox recipes/proof-general sandbox M-x package-install RET proof-general RET ```...
I think this is what you are looking for: (setq coq-indent-proofstart 0) (setq coq-indent-modulestart 0) Please confirm before I close the bug. Indeed this was asked by another ssreflect guy....
Agreed, buffer local would be cool. But how would you set it? Each time you open a file? Pretty painful. This is typically a setting that should be set by...
I confirm. It got removed in the refactoring of indentation. I will put this back quickly. Sorry for the inconvenience.
By the way is this still open? Do we want these variables buffer local?
Yes. But we should also fix #458.
Does the slowdown happen during the processing of the file or after it?
AFAIK there is no reason why overlays remain after retracting. Except performance maybe. But on the other hand dealing with hundreds of overlays (maybe a few thousand) should not be...