coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.5 error: Clause "in" expected in patterns over "match" expressions explicit "return" clause

From: Viktor Vafeiadis <viktor AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq 8.5 error: Clause "in" expected in patterns over "match" expressions explicit "return" clause
Date: Thu, 17 Mar 2016 17:52:36 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=viktor AT mpi-sws.org; spf=Pass smtp.mailfrom=viktor AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:vzVDixShdakhc9eVLQRJ2FAtndpsv+yvbD5Q0YIujvd0So/mwa64ZxyN2/xhgRfzUJnB7Loc0qyN4/CmATBLsczJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uLP04Y3nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAokxlUBBKN0hj0U5b4virh/r5j2SqGOtfeSKg1HC+99OFsUhC+23RPDCIw7GyC0p84t6lcuh/0/xE=

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

[Coq-Club] Coq 8.5 error: Clause "in" expected in patterns over "match" expressions explicit "return" clause, Viktor Vafeiadis, 03/17/2016
- Re: [Coq-Club] Coq 8.5 error: Clause "in" expected in patterns over "match" expressions explicit "return" clause, Tej Chajed, 03/17/2016