Без подразбиране в зависим модел на съвпадение с ssreflect

Струва ми се, че с ssreflect имплицитните полета на конструктора се превръщат в експлицитни полета, когато правим зависимо съвпадение на шаблони, и задаването на различни косвени опции не засяга това поведение.

Следният код е добре с Coq 8.6:

Require Import Coq.Unicode.Utf8.
Set Implicit Arguments.
Set Contextual Implicit.

Inductive Vec (A : Type) : nat → Type :=
  nil  : Vec A 0
| cons : ∀ {n}, A → Vec A n → Vec A (S n).

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons x xs => cons x (append xs ys)
  end.

Той спира да работи, когато импортирам ssreflect, защото изисква допълнително поле за шаблона cons в append:

From mathcomp Require ssreflect.

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons _ x xs => cons x (append xs ys)
  end.

Каква е причината за това и има ли начин все още да има имплицитни елементи в съвпадението на шаблони?