coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Calling things from a parent module into another module as neat as possible

From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
To: Milad Ketabii <ketabii.math AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Calling things from a parent module into another module as neat as possible
Date: Wed, 06 Jun 2018 09:14:22 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT chene.dit.umontreal.ca
Ironport-phdr: 9a23:Z9Y3uhE9LTMGrO1xhq1OPp1GYnF86YWxBRYc798ds5kLTJ7zpsmwAkXT6L1XgUPTWs2DsrQY07eQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDqwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJfH42ybIUPAeQDMulWoIbyu0ADrQeiCQS2GO/j1iVFimPw0KYn0+ohCwbG3Ak4EtwTrHTbstv1O70UUeuoy6fIyjPDb/VX2Tjj8ojDbxcsofSLXbJ2d8rRyFcgFxneg1uTtYLrJimZ2eoKvWic6epgSfivhHA9pAF1uDSi2Nshh5DPi4kIyV7E7T10zJs7KNGmUkJ3f8KoHZRKuy2EOIZ7Q9kuT390tCoi17ELt4C3cDIUxJg7yBPTceKLfoqS7h79W+udPzF1j29/dr2lnRa9602gx/X8Vsaq1FZKqTJIncXMtn8T0Rzc9NKLReZ8/ke9wzqPygXT6uZCIUAoj6rUNYQuwroqmpUPq0vPBi72mEPog6+Kbkgo5+al5/r9brn4upOROJV4hh/xP6kvgMCzH/g0PhALX2eB+OS80LPj/Vf+QLVPlvA2l67ZsJbcJcQauKG5GRRY0oc56xa4FTumzdEYnX4BLFJZYhKIkZLmO1XULP/kF/izm06snytzx/DaIr3hBY3AIWTEkLf4ZLpy90pcyBcowt1E/JJVCrQBIOrpVUPrtdzYCAU5Mw2uzOr9BtV9zNBWZWXaJ66dOa+aklKU7+guIqHYZ4IJsTz8Kr4g7uLupXA8kF4ZO6Ku2M1ERmq/G6FdP0iXaHykp9AHF2YHpEJqSevsjlyPSxZyXVH0Yoc74C0hBYuiS6zqENP+yIed1Tu2S8UFLltNDUqBRDKxL93dCqU8LRmKK8okqQQqEL2oSosvzxar7V+oyqBgaPfR/SsEr5/q0J5+7r+KzE1gxXlPF82Yllq1YSRshGpRF20X5oc5nGl6zEuZ3KF8xddxR4QKuqF5FzwiPJuZ9NRUTtD/XgWbIoWCSFugT5OqAC13U9c2xcMUbk95Xd6r3EjO

> The problem is that I need to use the name of Base in front of f1 and f2 at
> each instance by writing Base.f1 and Base.f2 . What I want is to simply
> write f1 and f2 wherever I wish and go through no problem.

BTW, I have grown to like those prefixes. When they get too verbose,
rather than importing the whole of Base.Base I often prefer to define
a local shorthand (like B) for it.

Stefan

[Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
- Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Sylvain Boulmé, 06/06/2018
  - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
    - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Pierre Courtieu, 06/06/2018
      - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Ralf Jung, 06/06/2018
        
        Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Pierre Courtieu, 06/06/2018
        
        Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Milad Ketabii, 06/06/2018
    - Re: [Coq-Club] Calling things from a parent module into another module as neat as possible, Stefan Monnier, 06/06/2018