From f9d4f732f2af7f706afbd97f53bbb020154375b3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 1 Mar 2000 11:05:00 +0000
Subject: New projects added

---
 html/projects/coqfile.html | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 html/projects/coqfile.html

(limited to 'html/projects/coqfile.html')

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>
-- 
cgit v1.2.3