The Coq mailing list

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

Hello, Dmitry.

Currently, debugging in proof session with little reduction steps
with or without coq-breakpoints is more or less enough.

What I asked about from the beginning: possibility to print text while evaluating term.
In form of ad-hoc macro or function with side-effect similar to trace from Haskell.
Maybe it is very easy to implement such function with OCaml plugin.

Example:

Definition double (n : nat) :=
    match n with
    | S n' => TRACE "S branch" (S (S (double n')))
    | O    => TRACE "O branch" O
    end.
Eval compute in double 1.
(* S branch \n O branch \n 2 *)

P.S. (Haskell, Debug.Trace) trace :: String -> a -> a.

Sincerely,
Kirill Taran

On Wed, Mar 12, 2014 at 5:09 PM, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

  Please describe what kind of tracing/debugging
you need.  Small example would be the best.

  As for cbv, it's not mandatory.  You can use
other tactics to reduce expressions: simpl,
compute.  Also you can reduce expressions
under "breakpoints".