blob: 03836398a2ec311646601ae6bc2dde7078931946 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
<h2>Multiple file handling support for Coq</h2>
<p>
Coq Proof General does not yet handle script management across file
boundaries, as do the LEGO and Isabelle versions. Script management
for multiple files means that whenever a file is viewed in the editor,
it is locked if it has been loaded into the current Coq session. It
may also mean that one can some file-level primitives of Coq, rather
than loading each file manually in the interface. This means that
complete proof scripts will not usually need to be parsed by
Proof General, solving one of the present problems with using
Coq Proof General.
</p>
<b>Skills:</b>
Some understanding of Coq implementation, co-operation with
the Coq developers to get any Coq modifications (if any) incorporated.
Some Emacs Lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
|
