The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

I would have thought the keyword "Unsafe" would have covered it, 
wouldn't it ?

Julien Forest a écrit :
> > 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
>
>