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: Théo Zimmermann <theo AT irif.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How do I make Hints available outside a section?
Date: Tue, 12 Jan 2021 11:05:52 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:sSvP1heTI0DMC0QFKsf2IRWTlGMj4u6mDksu8pMizoh2WeGdxcS+Yh7h7PlgxGXEQZ/co6odzbaP7Oa6BDBLucvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/PusQWjoZuJbo9xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJelXr4f/qFUOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSf67zKnSyjXEd/xZ2jb96I3Nch8/u/GMWKh/cczXyUIyEA7FklWQppLiPz6O1+QNqWmb7+R6WeKhkW4qsgd8qSWgyckwkIfGnJ4Vykza+iVjxoY4PcG1RVB/bNCrEZZduS+UOYV2T84tXWxlpTs2xL0atJO7fyUExpsqyh/cZvGHcoWG7BztWuaNLTl4hX9oeqyzihS0/EO9yeP8TtG53EtOoydKiNXAqHAA2hPJ5sWGV/dx5Fqt1DiM2gzL9O1IPUQ5mbDYJpMh2LI8iIYfvEfZEiPrmkj7j6mbfVg+9Oey8eToeLDmq4ecN4BqjgH+Nbwjms+4AeQiNQgOW3aU+fqm2L3++035QatKguQukqbDqpDaJN8bq6yjDw9byIYv8xe/DzG439QEhXQLMVZIdR2dg4T3O1zDL+r0APaij1i2jTtmyfPLMqXkAprXL3jDlLnhfax6605Z0Acz0dBf6IxTCrwaIfLzQE7xtNLCAh83KQy42/znB8ll1oMCRWKPBbeUP7/VsV+R/+4gP+2MZJIOtzvmMPgk5/vujWcjllMHfKmp24EXaHGiEfh8LUWZeymkvtBUOmAT9iE6Ueai3FaFSHtYY2u4d6M6/DAyToy8W9TtXIeo1YCBXSCMLJxTY21cD1mKFz+8a4WJXN8NciOcZMF7xG9XHYO9QpMsgEn9/DTxzKBqe6+NonVB6MDTkeNt7uiWrikcsDx5C8PHjzOOSHtzmm4WASIw3b46uUVny0zcl6Zi0aQBRI5joshRWwJ/DqbyiulzCtT8QAXEL4WIUleoBNu8U2hoEoABhuQWakM4IO2MywjZ1nv4AqUUmfqFHs5s/w==

Neither. That's a limitation. It could be overcome but this is far from trivial.

Le mar. 12 janv. 2021 à 09:18, Jim Fehrle <jim.fehrle AT gmail.com> a écrit :

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