The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

The "solution" I found is to define a new tactic :

<<<
Tactic Notation "dest" constr(X) "==" constr(Y) :=
  match goal with
    | H : context[ @eq_dec ?TYPE ?INST X Y] |- _ =>
      destruct (@eq_dec TYPE INST X Y)
    | |- context[ @eq_dec ?TYPE ?INST X Y] =>
      destruct (@eq_dec TYPE INST X Y)
    | |- _ => destruct (X == Y)

  end.
>>>

It still won't work if I have two occurrences of "x == y" with
different hidden parameters, but for now, it's not bad.


I might also try your solution of putting `{EqDec elt} only on
function that really need it.

Thanks!

Alexandre