The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

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.