The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 31/05/2016 17:27, Jonathan Leivent wrote:
> 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?

You simply get a parsing error, namely:

Syntax error: ')' expected after [constr:lconstr] (in [tactic:tactic_arg]).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature