The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

> I personnally have no problem with an Unsafe Fixpoint feature. It's 
> nothing worse than using "Axiom" anyway (plus it doesn't block 
> reduction, so it's even better). As long as when I Print an Unsafe 
> Fixpoint, I can see it is such (and more generally, that it's an 
> accessible information to the kernel).
The only difference between Axiom and Usafe Fixpoint is that any one is
(should be) aware that using Axiom is dangerous w.r.t. consistency. 
J