The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I frequently find myself writing

  match constr:Set with

    | _ => constr:(...)

    | _ => constr:(...)

  end

to get backtracking on type errors in constr-producing-Ltac, and then later changing it to constr:(Set) when the continuous integration fails to build it on trunk.  It's not a big pain to translate, but it might be nice to have a forward-compatibility script that I could run on my developments to make such forward-compatible-ensuring changes (and it would catch things like this, and maybe more complicated things too, if there are other such changes, e.g., it would have added [Require Import Coq.omega.Omega.] in the 8.4 -> 8.5 transition to files that needed it)

On Tue, May 31, 2016 at 11:27 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 05/31/2016 11:05 AM, Pierre-Marie Pédrot wrote:

... Likewise, for reasons I am not really sure to understand, it
forces you to write the ugly

constr:((x, y))

when parsing pairs.

On closer inspection, I found one instance of "constr:(x, y)".  But just one, no big deal.

An important question is - when 8.6 tries to parse a badly formed constr: such as "constr:(x, y)", what will the error message say?

-- Jonathan