coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Qualification confusion in module organization

From: Ramkumar Ramachandra <artagnon AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Qualification confusion in module organization
Date: Fri, 5 Jan 2018 16:47:46 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=artagnon AT gmail.com; spf=Pass smtp.mailfrom=artagnon AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f169.google.com
Ironport-phdr: 9a23:1Ej3ixFOzfbdWsQ4OG3/lJ1GYnF86YWxBRYc798ds5kLTJ78p8uwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZHo2zdY4PD+kcPeZdtYb9vUYFowekCgmpHuzg1j9IiWXw3aInyeQuCxzN0Qs6ENIUrHTbttr1NKEVUeCz16TIwjDDYOlX2Tf58oTHbhchofSVUL92bMHfylEvGhvbglmMrYHpJTCY2+QXv2SG7udsSPijh3Mmpgx1pDWk290ihZPTho0Pz1DJ7SV5z5gxJd2/UEN7ZMSrEJpUty2DN4p3TN8uT3hmuCony7ALvYS3fCcNyJQgyB7fb+KIf5KU7RLkUeadOTZ4hHR7d7Kjnxu+71Ssx+nmWsS30FtGtDdJn9jRunwXyhDe68yKRuN4/ki72DaP0w7T6vtDIUAxjafUMYQhwqIqmZoct0TDGSn2lV75jK+TbEok++yo5/77bbXho5+QL5V0hR3mMqQyhsy/Bvw1PRQJX2iC4OizyLnj/VDiT7hRlf03kqzZsIjAKsgBp665BRVV0oc55BqlATemyodQoX5SJ1VcPRmDkoLBOlfUIfm+A+3srU6rlWJRzvXFI7joGN33J33Km7foe7pn4gYIwRAvxN9Z4JR8BbQIIfa1UUj04o+LRiQlOhC5lr60QO520ZkTDDqC

Hi,

I'm having a lot of difficulty using a lot of the functions listed in the Standard Library, due to some qualification confusion.

For instance, how do I use add_in from FMapAVL? Both M.add_in and M.Raw.add_in don't seem to work. Where can I find a systematic guide to module organization? CPDT doesn't seem to cover it (I've gone through ~4 chapters).

Thanks.

Ram

[Coq-Club] Qualification confusion in module organization, Ramkumar Ramachandra, 01/06/2018