coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic inlining?

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactic inlining?
Date: Mon, 1 Feb 2016 01:28:56 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT mo68.mail-out.ovh.net
Ironport-phdr: 9a23:1y9uTRAWpfNwKnbnz9OoUyQJP3N1i/DPJgcQr6AfoPdwSP74oMbcNUDSrc9gkEXOFd2CrakU1KyO4uu5CTdIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbqqtaKM14ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jd2wGkx9FSyRE6pHhFsP0uyr+nu90yCifMMH7S70vHzq4ufQ4ACT0gTsKYmZquFrcjdZ92fpW

Hi Beta,

The syntax was changed to :

Definition test : nat := ltac: (exact 1).

I believe it is documented in the CHANGES file.

Cheers,

Maxime.

On 02/01/16 01:26, Beta Ziliani wrote:

Dear all,

In Coq 8.5beta1 it is possible to write the following code:

Definition test : nat := $( exact 1 )$

However, in Coq 8.5 it complains saying that $( is an undefined token.
Did it change? Is it in the ref-man? Where?

Thanks a lot,
Beta

[Coq-Club] Tactic inlining?, Beta Ziliani, 02/01/2016
- Re: [Coq-Club] Tactic inlining?, Maxime Dénès, 02/01/2016
  - Re: [Coq-Club] Tactic inlining?, Beta Ziliani, 02/01/2016