The Coq mailing list

[frederic.blanqui AT loria.fr]

On Fri, 13 Jun 2008, 
frederic.blanqui AT loria.fr
 wrote:

> Hello. As it is well known, many function definitions are rejected by Coq 
> since they do not pass Coq termination checker which accepts only 
> structurally terminating functions. Would it be possible to add a new 
> command line option to coqc that would disable the termination checker?

Instead of a command line option, it would be better to have a command like 
"Unsafe Fixpoint" to disable the termination check locally and keep a trace of 
this in the file itself.