Pierre Courtieu writes:
Is there a reason why emacs completely hangs when auto compilation is
You mean emacs is locked until compilation is finished and all
asserted items are in the queue region? Or do you mean something
Emacs is locked because I avoided all synchronization trouble and
call coqdep and coqc synchronously. All this happens before the
asserted items are put into proof-action-list.
This is not optimal, but for a first version it is hopefully ok.
ProofGeneral-devel mailing list