diff options
Diffstat (limited to 'todo')
| -rw-r--r-- | todo | 8 |
1 files changed, 0 insertions, 8 deletions
@@ -389,14 +389,6 @@ X pbp code doesn't quite accord with the tech report; in particular it C fix Pbp implementation (10h) -B `lego-get-path' assumes that LEGOPATH has been set in the - environment. This is not likely to be the case with the current lego - shell script. Proof General needs to query the LEGO process as part - of `lego-process-config' e.g. by - sending (a yet to be implemented command) LEGOPATH. The output could - be analysed with the help of a LEGO specific extension of - `proof-shell-process-urgent-message'. (1h tms) - B Equiv, Next,... aren't handled properly, because LEGO does not refresh the proof state. Perhaps it would be easiest to get LEGO to output more information in proof script mode (2h) |