The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I am trying to explore behaviour and fix a patch, so I am using debugger.

I have read dev/doc/debugging.txt and as it says I use "ocamldebugger-coq" wrapper, but CLI version (not with emacs). Coq is configured with "-local -debug".

I can't set breakpoint on function I want -- separate_extraction from extract_env.ml.
I tried "break separate_extraction" and "break Extract_env.separate_extraction", but these two give me "Unbound identifier <...>".
I have seen text in manual that the function has to be computed and assigned to identifier, so I tried also advance execution to necessary point with "goto <time>".

Command "break @ Extract_env <line>" gives message, that there are no events,
whereas "list Extract_env" succeed.

So, could anybody provide me with little example about how to set break point in command line for any Coq internal function?

Sincerely,
Kirill Taran