The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

P.S.: and there's a workaround too:

<<
Section Check.
  Variables  (n : nat) (P : { i | i < n } -> bool).

  Program Fixpoint check_n (p : nat)
    (H : forall (i : { i | i < n }), i < p -> P i = true)
    {measure (fun i => n - i) p} :
    Exc (forall (p : { i | i < n}), P p = true) :=
    match le_lt_dec n p with
    | left _ => value _
    | right cmp =>
      if dec (P p) then
        check_n (S p) _
      else
        error
    end.
>>