coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] curious behavior of "Locate" command

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] curious behavior of "Locate" command
Date: Wed, 8 Jun 2016 09:15:03 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:Y4N/FR9+kaFEd/9uRHKM819IXTAuvvDOBiVQ1KB91+8cTK2v8tzYMVDF4r011RmSDdSdtKkP1reempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lS8iN1I/qiqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzoSYqK630AZV0Xjl8NKAzM8R33Wt+luS/3s+d7xG+CPNHeQrU9WDDk5KBuHky7wBwbPiI0pTmEwvd7i7hW9Uqs

On 2016-06-08 09:07, Matej Kosik wrote:
> However, when I try to ask Coq where is "_ ~ _" defined, I get a reply:
>
> Unknown notation

Note that `Locate "_ ~ 0"` works.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] curious behavior of "Locate" command, Matej Kosik, 06/08/2016
- Re: [Coq-Club] curious behavior of "Locate" command, Clément Pit--Claudel, 06/08/2016
  - Re: [Coq-Club] curious behavior of "Locate" command, Tej Chajed, 06/08/2016
    - Re: [Coq-Club] curious behavior of "Locate" command, Matej Kosik, 06/08/2016
- Re: [Coq-Club] curious behavior of "Locate" command, Guillaume Melquiond, 06/08/2016