coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic inlining?

From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Tactic inlining?
Date: Sun, 31 Jan 2016 21:31:13 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=None smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT famaf.unc.edu.ar
Ironport-phdr: 9a23:G4E3XxGT7Q0lVKdaq921HZ1GYnF86YWxBRYc798ds5kLTJ75oMqwAkXT6L1XgUPTWs2DsrQf27WQ6/GrADxbqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0o8yYOlUTzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazXwFGk4SjxAAVwPC9VTxWor7mir8rOt0nieAa57YV7cxDB6v864jeh7siS4BNnZt+nPWjs15iqNzrhukrhI53ojfJoyZKbx3ZPWOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==

D'ough, I even saw the discussion (I think in coq-dev). Thanks!

On Sun, Jan 31, 2016 at 9:28 PM, Maxime Dénès
<mail AT maximedenes.fr>
wrote:
> 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