From 9ae40ab19a1aa2a94f0def7e74a652ebb82417a9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 9 Mar 2000 07:48:32 +0000 Subject: Tweaks --- html/projects/coqfile.html | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'html/projects') diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html index 03836398..35d48eb1 100644 --- a/html/projects/coqfile.html +++ b/html/projects/coqfile.html @@ -4,12 +4,14 @@ 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 +may mean that Proof General can make use of the file-level primitives +of Coq, so that the user doesn't have to escape the interface, +or carefully load each file and its dependencies. This also means that +complete proof scripts will not so often need to be interpreted by +Proof General, solving one of the present bottlenecks with using Coq Proof General.

+

Skills: Some understanding of Coq implementation, co-operation with the Coq developers to get any Coq modifications (if any) incorporated. -- cgit v1.2.3