coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I make Hints available outside a section?

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I make Hints available outside a section?
Date: Tue, 12 Jan 2021 00:17:47 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f48.google.com
Ironport-phdr: 9a23:cZtIrh/V85a2uf9uRHKM819IXTAuvvDOBiVQ1KB42+0cTK2v8tzYMVDF4r011RmVBNqdsa8ewLuM+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanf79/LAu6oQrVu8UInIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahcN+jK1ZoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VoY38p1sLsBCwBRejBOP1yj9MmHD9wKo30+YgEQHDxgAgEcwBsHTOrNXxKqgfSu+1zKzSwjXCa/Nawyvy6I/Nch04p/yHQL1/f9bLx0Y1CwPFkkufqZbjPz6NyukAsHaW4u5vWO+uj2MqqR19ryahyMooloXEmoYYxkzF+Ch3wYs4O8O1RFJ/bNOgEpZduC+UOpZ5TM4/XWxkpCA3waAFt56jZCUG1ogryhrFZ/GEc4WE+A/vWeeQLDtii39oe7SyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx50ah2TGS2wzK5OFJLkM5mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue29+TqeqvqqoOYOoNuiQzzMr4iltG+DOk5KAQDUGuW9fy51LL5/E35RLtKjucxkqncqJ3aJ8UbpqujDw9bzIkj6wy/DzO439kDknkHKUhKeBODj4TzJ17OJ/X4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoCfkgr9DjjWU9lBdJf6ism5UaaGq8E9xpJkyYZTznhdJXQjRChRY3UOG/0A7KajVUfXvnB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPPzJJD1mNFTHjcIDWAq5QOhLXGddol3k/bZbkU5UojEj8uwrzyr4hJe3RqHVB6MDTkeNt7uiWrikcsDx5C8PHjjOIRmBw22IPHno4gPA5rkt6xVOOl6N/hq4AGA==

Not supporting global in sections--is that a bug or a feature?

[Coq-Club] How do I make Hints available outside a section?, Agnishom Chattopadhyay, 01/11/2021
- Re: [Coq-Club] How do I make Hints available outside a section?, Jim Fehrle, 01/12/2021
  - Re: [Coq-Club] How do I make Hints available outside a section?, Théo Zimmermann, 01/12/2021
    - Re: [Coq-Club] How do I make Hints available outside a section?, Jim Fehrle, 01/12/2021
      - Re: [Coq-Club] How do I make Hints available outside a section?, Théo Zimmermann, 01/12/2021
        
        Re: [Coq-Club] How do I make Hints available outside a section?, Agnishom Chattopadhyay, 01/12/2021
        
        Re: [Coq-Club] How do I make Hints available outside a section?, Jim Fehrle, 01/12/2021