coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Printing the call-stack of coqc on error

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Printing the call-stack of coqc on error
Date: Mon, 28 Jan 2013 14:57:16 +0100

On 27/01/2013 21:04, Jason Gross wrote:
> Is there a way to get Coq to print it's (ocaml) call stack whenever it
> prints "Error: ..."?

I've just added a backtrace printer in the trunk for the [Anomaly] case,
as a proof of concept. I'm not sure whether this is very meaningful in
the [Error] case, because of the many ways it tends to be caught, but I
can also do this indeed.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/27/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Arnaud Spiwack, 01/28/2013
  - Re: [Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/28/2013
- Re: [Coq-Club] Printing the call-stack of coqc on error, Pierre-Marie Pédrot, 01/28/2013
  - Re: [Coq-Club] Printing the call-stack of coqc on error, Gabriel Scherer, 01/29/2013
    - Re: [Coq-Club] Printing the call-stack of coqc on error, AUGER Cédric, 01/29/2013
  - Re: [Coq-Club] Printing the call-stack of coqc on error, Jason Gross, 01/30/2013
    - Re: [Coq-Club] Printing the call-stack of coqc on error, Pierre-Marie Pédrot, 01/30/2013