The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

That is a bug. Maybe if you include more information in some match-with-end pattern, you can get around it. Here are some examples:

(* without wildcards, with as-in-return, type-checks *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 in _ <= n2 return pred n1 <= pred n2 with
  | le_n      => le_n (pred n1)
  | le_S n2 H1 =>
    match n2 as n2 return pred n1 <= pred n2 -> pred n1 <= pred (S n2) with
    | 0   => fun H2 => H2
    | S n3 => fun H2 => le_S (pred n1) (pred (S n3)) H2
    end (le_pred n1 n2 H1)
  end.

(* without wildcards, without as-in-return, doesn't type-check *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 with
  | le_n      => le_n (pred n1)
  | le_S n2 H1 =>
    match n2 with
    | 0   => fun H2 => H2
    | S n3 => fun H2 => le_S (pred n1) (pred (S n3)) H2
    end (le_pred n1 n2 H1)
  end.

(* with wildcards, with as-in-return, type-checks *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 in _ <= n2 return pred n1 <= pred n2 with
  | le_n => le_n _
  | le_S n2 H1 =>
    match n2 as n2 return pred n1 <= pred n2 -> pred n1 <= pred (S n2) with
    | 0 => fun H2 => H2
    | S _ => fun H2 => le_S _ _ H2
    end (le_pred _ _ H1)
  end.

(* with wildcards, without as-in-return, stack-overflows *)
Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 :=
  match H1 with
  | le_n => le_n _
  | le_S n2 H1 =>
    match n2 with
    | 0 => fun H2 => H2
    | S _ => fun H2 => le_S _ _ H2
    end (le_pred _ _ H1)
  end.