diff options
| author | David Aspinall | 2000-03-01 11:05:00 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-03-01 11:05:00 +0000 |
| commit | f9d4f732f2af7f706afbd97f53bbb020154375b3 (patch) | |
| tree | be06f9d71986966e7fe114ad5acf92e8adfb1053 /html/projects/coqfile.html | |
| parent | 1eb942a57d39a4e1d5c123cd0cf6c60a720fa47c (diff) | |
New projects added
Diffstat (limited to 'html/projects/coqfile.html')
| -rw-r--r-- | html/projects/coqfile.html | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html new file mode 100644 index 00000000..03836398 --- /dev/null +++ b/html/projects/coqfile.html @@ -0,0 +1,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> |