Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Namespace Modules inside Sections

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Namespace Modules inside Sections


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>, Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • Subject: RE: [Coq-Club] Namespace Modules inside Sections
  • Date: Sun, 27 May 2018 13:16:45 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
  • Ironport-phdr: 9a23:9HPhDBURFgrzNfPMPv+G5Mf4fbLV8LGtZVwlr6E/grcLSJyIuqrYbRSHt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/VxcK7GYdMVXm5MUtpNWyBdAI6xaZYEAeobPeZfqonwv1UCowa5BQayC+Pv1iVIhnju3aEizu8vFgDG0xAgH90UrnvUqNv5P7oVXOCwzanH0TXDYOlI1jf58oTIaRchru+DXbJsa8rRzlEvGhjEjlWWtYzqITeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4IUzFDE6Tt2wIIvKdKlVkF2Z8OvHphItyyCKod7TMwvT3t1tCs0xbAKo4O3cSYLxZg9yRPTduSLf5WJ7x/tTuqcLzl1iGh7dL+xgxu+61Wsx+7iWsWszVpHry5InsPSun0N2BHf8NaLRuFg8kqi2zuC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBir2mErsg6OKd0go4Omo6+L7Yrr4op+QLZN7igb7Mqg2m8y/B/o3MhQWUmSG9+mx26fv8VD3TbhFlPE6j6fUvZHAKckVu6K1GwpV3Zwi6xa7ATemytMYnXwfIVJAeRKIk4jpNEvQL/D8F/u/mFOsnylkx/DaJL3hBY3NI2PCkLfnYbZy9UpcxBAvwtBY4pJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa78l5AQcTWzGulsC0Sfe3vlxNkbWy9etQ0nCefulVeqUDhJZn/0UbhqonkSAoKnFofORciEhrWH0G/vF5dWZ3tGB1PKGHHhcYnCWvYQZwqdJ8ZglnoPUr33GKE70hT7/jT9xrV7NO3MvmU9tJnj3dVxraWHkBA59TV5C4KG1GyCU3tzhksJQSM72OZ0pkkrmQTL6rRxn/ENTY8b3PhOSApvbceNndw/MMj7X0f6RvnMTV+nRtu8BjRoF4AwxcMDZwB2HNDw10mfjRrvOKcckvmwPLJx6rjVhiGjJsBhxnKA364k3QF/H5l/cFa+j6s6zDD9Qo7El0LAyPSveq1EgmjM8nuOySyFu0QKCAM=

Dear Ralf,

I guess what Abhishek meant is that it would be useful to have namespaces,
which don't do anything fancy at all, but just prepend "name." in front of
any name you define in its scope. That's it. I guess Abhiskek would like to
have Import and Include work as with files. And I guess It would be tricky to
handle OCaml export.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928



Archive powered by MHonArc 2.6.18.

Top of Page