Often it matters that Coq places a type in Prop rather than in Type. Here is an example where a type ascription is needed to place a match in Prop.

```
Inductive even: nat -> Prop :=
| evenB: even 0
| evenS: forall n, even n -> even (S (S n)).
Goal even 1 -> False.
Proof.
refine (fun a => match a in even n
return match n with 1 => False | _ => True end : Prop
with evenB => I | evenS _ _ => I end).
Qed.
```

The term doesn’t type check without the ascription since Coq places it in Type, which invalidates the match on the proof `a`

. This type checking behavior has the unfortunate consequence that the smart match

```
Goal even 1 -> False.
Proof.
refine (fun a => match a with end).
Qed.
```

doesn’t type check. I don’t know how to annotate the smart match so that it type checks.

So my question is whether this is a design decision or a bug?

Thanks in advance,

Gert