The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

On Fri, Feb 21, 2014 at 10:26 PM,  
<julien.forest AT ensiie.fr>
 wrote:
> Long answer : Can you please fill a bug report at
> https://coq.inria.fr/bugs/ so that I can treat the problem as soon as I
> come back. I won't be at work next week.

I will file a bug report. Is the following also a bug? If so, should I
submit one or two bug reports?

http://pastebin.com/NN8TBD1E

Require Import Recdef.

Inductive formula :=
| atom : formula
| ex   : nat -> formula -> formula.

Parameter substitution : formula -> nat -> nat -> formula.

Fixpoint complexity P : nat := match P with
| atom     => 0
| ex _ P   => complexity P + 1
end.

(*
failure in proveterminate

Error: Found a lambda which body contains a recursive call. Such terms
are not allowed
*)
Function truth P {measure complexity P} : Prop := match P with
| atom     => True
| ex   n P => exists m, truth (substitution P m n)
end.