The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

No there isn't. Yet.

A few thoughts. Originally that was hard to do because Coq could be compiled with old version of OCaml which didn't have a backtrace support, it's not the case anymore so we could add support for backtraces. Note that Coq needs to be compiled with -g for that to work. Also, there is a high chance that the backtrace be mangled: Coq uses a lot of dynamically loaded plugins, which may cause some issues (I'm not sure), and more importantly, it uses exceptions a lot, with a pretty complex control-flow, and OCaml has a fairly roundabout way to trace errors, which doesn't quite like complex control flows.

On 27 January 2013 21:04, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

Is there a way to get Coq to print it's (ocaml) call stack whenever it prints "Error: ..."?

Thanks.

-Jason