The Coq mailing list

[t x <txrev319 AT gmail.com>]

Consider the following minimal failure example:

Notation "'bFoo' A 'eFoo'" := (A + 2).

Eval simpl in (bFoo 2 eFoo).

Eval simpl in (bFoo false eFoo).

Right now, all I get is: a complaint of "got bool while expectig Z"

This is not particularly useful on larger examples.

The process appears to be:

[1] (bFoo false eFoo)

[2] (false + 2)

[3] type-check

[4] report type check error

Is there a way to put in a [2.5] --> print out what _expression_ is, before it is type checked?

Seeing "(false + 2)" would make debugging much easier than just a "got bool; expected Z"

Thanks!