The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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