The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

On Wed, 8 Sep 1999, Eduardo Gimenez wrote:
> Unfortunately, there is no written formal description of the
> modifications introduced in the guardedness condition, but you will
> find an illustrative example at the end of this mail.  There were no
> modifications to cofixpoint definitions.
> 
> Coq's code evolves faster than we write new versions of the manual, so
> it's very likely that the current manual is outdated.

This is reasonable, but the new (and weaker) guardedness condition has
been proved to be consistent, hasn't it?

So somewhere there *should* a formal study on this... is it accessible?

Thanks anyway,
- Marino