The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Stéphane,

Le 22 sept. 09 à 09:54, Stéphane Lescuyer a écrit :

> Hi Bruno,
>
> Thank you for your explanation, this makes perfect sense indeed, once
> you know what's going on under the hood. The issue here is how do you
> know the expression which is actually fed to the typechecker ? My
> error message only shows the typing context and not the whole fixpoint
> body :
>
> Recursive definition of no_hole is ill-formed.
> In environment
> no_hole : forall S : signature, context S -> Prop
> S : signature
> c : context S
> ...
> Recursive call to no_hole has principal argument equal to
> "a1" instead of cs.
>
> So I can actually see the two cs, cs0 and the corresponding a, a0
> which can help understand what's going on, but is there any option
> that I'm unaware of which displays the whole fixpoint body ? That
> would be pretty useful in such circumstances.

I added this info to the message in the trunk, it will be part of the
next version.

-- Matthieu