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
    proof-shell-exit-in-progress. When
    coq-switch-buffer-kill-proof-shell sees this it refrains from
    calling proof-shell-exit recursively.


ProofGeneral-devel mailing list

Reply via email to