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: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I make Hints available outside a section?
Date: Tue, 12 Jan 2021 07:11:29 -0600
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:4eJ/KBFuChh+pEbpOYF4nZ1GYnF86YWxBRYc798ds5kLTJ7zocywAkXT6L1XgUPTWs2DsrQY0rqQ6/irADVIoc7Y9ixbL9oUD15NoP5VtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLucQanIhvJrwtxhfVrXdEZvlazn5sKV6Pghrw/Mi98INh/ihKp/4t68tMWrjmcqolSrBVEC4oOH0v6s3xshnDQwqP5n8CXWgTjxFFHQvL4gzkU5noqif1ufZz1yecPc3tULA7Qi+i4LtxSB/pkygIKTg0+3zKh8NqjaJbpBWhpwFjw4PRfYqYOuZycr/bcNgHQ2dKQ8RfWDFbAo6kYIQPAegOM+ZWoYf+ulUAswexCBK2C+/z0DJFnGP60bE43uknDArI3BYgH9ULsHnMsNj1O6ESUeGuzKnIyjXDau5d1Cn96IfSbhAhvfaMXapqfsXMyUkuFxnKj1WNooHiJTyV2eINs2mA7+pgUuKvjnUqpB10ojiu3MsjkJXGipgUylDC7Ch0xps+KtKkRkBhe9GkDIdQuD+AN4twWs4sQ3xltDomxrAJvZO3YSgHxZs7yhPbdfCKc4eG7g/tWuufJTp1hGxodbK/iRuy8Uat1PPxW9ep3FtLrydInNrBu3YQ3BLQ8siKUuZx8lmv1DqV1g3e5PtILV4omafVMZIt3KM8moQLvUjdAiP7nF/6gayWe0k+5+Sl6uXqbq/mq5KSMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEsjqbZtZHaKd4BqaGlGQNV04Aj5w6+DzegztsYgWEKIE9bdB+JlYTkOl/DLOrmAfujjVmgiilny+3YMrH5B5XCNHnDkLPvfbZn7E5czRI+wspQ55JSC7EBO/LzWkj0tNHDEhA5Ng20z/z9B9phzI8eWGSPDreDMKzOqV+I+v4vI+6UaYAJvzb9MuEp6OLqjX8kglAQZrKp3JsSaHCgBPtqOUSZYXz2gtcAC2gGpAQ+TPa5wGGFBDVUfjO5W782zjA9EoOvS4nZFa63h7nU9Si9H4ZWYWUOIVCFDWvvb4yIW+YFeWrGK8BnkycEUr2JQIogkxil8g78nek0ZtHI8zEV4MqwnON+4PfewElrqW5ESv+F2mTIdFla23sSTmZvjqt6oAp0wRGC1/og2q0KJZlo//pMFzwCG9vZxu1+Bcr1X1uYLNyMSRCvSZOnB2NoF49j85o1e094Xu6aoFXD0i6tWuFHkrWKANo/96Oa1nO3JsAvk3s=

As noted by you guys, Global works on Instances but not Hints.

So, what is the best practice to manage Hints?

On Tue, Jan 12, 2021, 04:06 Théo Zimmermann <theo AT irif.fr> wrote:

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