Paolo Herms <paolo.he...@lri.fr> writes:

   Processing a coq file within emacs means feeding the file to
   coqtop step by step. Compiling the file with coqc does pretty
   much the same thing [...]

Thanks for the clarification. I would say the
processing-twice-problem is somewhat orthogonal to detecting
out-of-date vo files. The latter gives correctness and is also
important when you update files outside of emacs. The former is
an optimization problem, which I would approach later.

>From my experience with PVS I would hope that one can get
reasonable performance by skipping proofs when reprocessing files
during development. 

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to