The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Jonathan Leivent 
<jonikelee AT gmail.com>
 writes:

> That's great!  Inference of pattern matching annotations is nice,
> although I'm confused about when to anticipate them.  Also, too bad I
> can't get similar support via destruct f, g - which is what I end up
> doing most of the time anyway.

Well, destruct will work if you actually state the more general lemma:

From Coq Require Import Eqdep Eqdep_dec.

Inductive Foo : unit -> Set := foo : Foo tt.

Lemma unit_dec (x y : unit) : {x = y} + {x <> y}.
Proof. decide equality. Qed.

Lemma foo_eqd w1 w2 (f : Foo w1) (g : Foo w2) : eq_dep _ _ w1 f w2 g.
Proof. now destruct f, g. Qed.

Lemma foo_eq (f g : Foo tt) : f = g.
Proof. now apply (eq_dep_eq_dec unit_dec), foo_eqd. Qed.

which IMO is a good idea to do, even if a bit cumbersome.

E.