Pierre Courtieu <pierre.court...@cnam.fr> writes:
2011/9/10 Erik Martin-Dorel <erik.martin-do...@ens-lyon.fr>:
> 3. Finally, it seems the function `proof-shell-exit' raises
> systematically an unexpected error.
> To reproduce it, run the (Coq) prover, then try:
> [M-: (setq debug-on-error t) RET]
> [C-c C-x]
I have noticed this too. This is recent. I have put this in trac.
The problem is coq-switch-buffer-kill-proof-shell and that
proof-shell-kill-function does not take into account that a
prover might get killed when scripting is deactivated. For more
details see #421.
If nobody objects, I'll adopt solution 1 (see #421 for solution 2):
Inside proof-shell-kill-function set a global variable
coq-switch-buffer-kill-proof-shell sees this it refrains from
calling proof-shell-exit recursively.
ProofGeneral-devel mailing list