coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic inlining?

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Tactic inlining?
Date: Sun, 31 Jan 2016 21:26:31 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:8U5fWRLMOiSZto7uCdmcpTZWNBhigK39O0sv0rFitYgULPvxwZ3uMQTl6Ol3ixeRBMOAu60C07ud6vC7EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35vxj7H5os2IKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJo5RT3q3aZvSRbuiW9TPTMl+UnSks01l71A5hW7qEoskMbvfIiJOa8mLevmdtQASD8EB54JWg==

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