The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

It looks like you're looking for cases of context[eq_sym eq_refl] based on my limited understanding of explicit dependent matches, in which case the following is accepted by Coq (tested on a recent build of v8.5):

Ltac des_eqrefl :=

  match goal with

    | |- context[match ?X in (_ = id) return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>

    let EQ := fresh "EQ" in

    let id' := fresh "x" in

    generalize (Logic.eq_refl X); generalize X at 1 3;

    intros id' EQ; destruct id'

  end.

On Thu, Mar 17, 2016 at 12:52 PM, Viktor Vafeiadis <viktor AT mpi-sws.org> wrote:

Hi,

I am trying to upgrade my developments from Coq 8.4 to 8.5 and I have the following basic tactic that used to work well on 8.4, but fails on 8.5 with the  error message:  Clause "in" expected in patterns over "match" expressions with an explicit "return" clause. Does anyone know why this is the case, and whether there is any workaround?

Ltac des_eqrefl :=
  match goal with
    | |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
    let EQ := fresh "EQ" in
    let id' := fresh "x" in
    generalize (Logic.eq_refl X); generalize X at 1 3;
    intros id' EQ; destruct id'
  end.

Thanks,

Viktor