The Coq mailing list

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

Thanks, coq-breakpoints looks as what I searched.

Also, as I understand it provides not so much --
"debugging" is possible with plain "cbv" in proof session
(but not very comfortable); I didn't know it is possible.

Sincerely,
Kirill Taran

On Wed, Mar 12, 2014 at 3:21 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

For tactics:

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#sec469

For the rest,

https://sympa.inria.fr/sympa/arc/coq-club/2013-03/msg00137.html

might help.

• From: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
• To: coq-club AT inria.fr
• Subject: [Coq-Club] Announce: coq-breakpoints
• Date: Thu, 21 Mar 2013 13:18:47 +0200

=====THREAD MESSAGE CONTENT=====
Hello.

I wrote a small library [1] that allows one to use "breakpoints"
(expressions that are not reduced automatically) in Coq code,
which proved to be useful to debug the code.

Examples:

https://bitbucket.org/gds/coq-breakpoints/src/tip/Bp_examples.v

Documentation:

https://bitbucket.org/gds/coq-breakpoints/raw/tip/README

Repository (www / mercurial):

https://bitbucket.org/gds/coq-breakpoints



[1] -- strictly speaking, it's not a library, just one file
"Breakpoints.v" that can be added to a project.

2014-03-12 10:36 GMT+01:00 Kirill Taran <kirill.t256 AT gmail.com>:

Also, maybe there are any tools/ways to debug coq development?
"Trace" would be useful, but I didn't find it.

Sincerely,
Kirill Taran

--
.../Sedrikov\...