coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with defining a new vernacular command

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem with defining a new vernacular command
Date: Thu, 03 May 2018 19:30:51 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:mWlHxRWBjmJnZ5BFSzBRGVz9wMbV8LGtZVwlr6E/grcLSJyIuqrYYxGBt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2ycZYBD+0PPehWrYbzpFUBohSiCgejH+7v1iZIi2Xq0aEmyeksEwfL1xEgEdIUt3TUqc34OqgXUeC0yKnIzDLDYOtS1zjj84jQaAshrumNU71qdcrRzVcgFwzCjlqItYHlJTKV2f4Ws2OG6OdvS/miimEkpg1tuDSvwd0siobQi48T11vK9j15zZ4oKdC7S0N3e8CoHIVRui2AKod7QN4uT3t1tCs01LEKoZ22cSkQxJkmxRPTcfiKf5KV7h7/SOqcJypzimh/d7KlnRmy9FCtyu3iWcmw11ZHtiVEn9rQunwX0BzT8MeHRuN8/kenxzmPyxje5vxHLE03j6bXNYAtz78qmpYOs0nPAzX6lFj4gaOIbkkk//Kn6+XjYrXovJ+cMIp0hxngPak1lc2yAvg0PhIJX2iB9uSwzKfj8lHhQLVWkv02lbHUv4zdJcQCv6K2HwtV0ps45BukFDen0NEYnWEdI15feRKHiZLpO1DUL/ziA/e/mQfkrDA+6PlFIrTnSrrMKnLOiqupKbl05lJVzkw8zNRV6ohIIqoCMenwW0r0ucaeCBIlZV+a2eHiXfh414cfXlWtD7QLK5T9uFuM6+0oFMCWZYYO8GLwA+h1v7jpl3BvygxVRrWgwZZCMCPwJf9hOUjMJCO02o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdttCFrUMShF4iRH9nx0ozE5z+yG9htXk4DEkqFQCX4J93CXO0DOnrLf51R1wccXL3kcLcPkBGjsAirmao3dqzT4CJK7J8=
Organization: X80 Heavy Industries

Gaëtan Gilbert
<gaetan.gilbert AT skyskimmer.net>
writes:

> Emilio might have more to say about this / I might have misunderstood
> something or said something unclear.

I think that's pretty much it, using an mlpack will put the modules into
their own namespace which is very much recommended.

E.

[Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
- Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
  - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
    - Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Emilio Jesús Gallego Arias, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof Bornebusch, 05/04/2018