The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Yes, I'm using ProofGeneral. I'm not sure how I installed it off the top of my head... I'd like to use some kind of package manage to facilitate keeping it up to date. Are there instructions anywhere to follow to make sure that the install of proof general goes well?

On Thu, Jul 9, 2015 at 3:38 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 07/09/2015 02:50 PM, Kenneth Adam Miller wrote:

Abhishek, I tried your technique by just pasting in what you gave to start
a new goal. The goal showed up, but the match statement didn't print
anything at all.

Kenneth,

Are you using ProofGeneral?  If so, note that non-latest versions of PG have issues with (among other things) properly handling and printing idtac messages from Coq.  You might be hitting this. Personally, I keep my PG updated to the latest CVS development version (:pserver:anon AT cvs.inf.ed.ac.uk:/disk/cvs/proofgen) - which, thanks to Pierre Courtieu, works much better with Coq than previous releases.

-- Jonathan