Opened 11 years ago

#464 new defect

proof script not displayed after startup

Reported by: coquser Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc:

Description

(I'm Dan Grayson <dan@…>)

I'm adapting pg under emacs to a new proof assistant that I'm writing (see https://github.com/DanGrayson/checker), and have just gotten started. The first problem was that after pg started scripting my proof script, the proof script buffer would disappear about the same time the *goals* and *response* buffers were displayed. I tracked the problem down to the function proof-display-three-b receiving nil as its first argument (why, I don't know), and "fixed" it as in the attached patch.

Change History (0)

Note: See TracTickets for help on using tickets.