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: Mon, 11 Jan 2021 17:53:22 -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-f47.google.com
Ironport-phdr: 9a23:QoYRVxEKS1CfUPUDi0gDf51GYnF86YWxBRYc798ds5kLTJ7zoc6wAkXT6L1XgUPTWs2DsrQY0rWQ6f26EjZRqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswncttcajYR8Jqs11xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMODkk/mHKkcxwlLxUrw69pxJxxI7UZZuaNPt4fqjAed8XSm5MUsNXWidcAI2zcpEPAvIOMuZWrYbzp1UAoxijCweyGOzi0SVHimPs0KAgz+gtDQPL0Qo9FNwOqnTUq9D1Ob8WX+C0yanD0DXNYO1W2Tfn7IjHbA0qrPaOXbJxdMrd00cvGB3FjlWKrYzqISiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhYbViIwP0F/E6Tl5z5gvJd2+UEN2fNGpHYdQuSyGK4Z4TccvTm50tSg617EKpIC2ciYFxpk72xLSaOGKfYaI7x/9UOucLyp0iXJqdr+jhBu88Uitx+vhXce611ZKqzBKktjKtn0V2BzT69SHSvtg/ki6wzqP1gfT5+dZKk43jarWM4AtzqI0m5YJsknOHjX6lFj3gaKXbEkp9eql5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxALX2eB+OS80KTv/Uz+QLlXl/E2nKbUvZLAKcQUoa65BABV0oI95BqlEzim19EYkWEGLFJDZh2Hk5DkN0/SLP38F/uygFShnC12y/3HP7DtGJrAI3rbnLfkZ7l96kpcyAQpzdBY4pJZErMBIPP2WkPrutzXEB85Mxaww+n5E9h92YYeVniOAq+dKq/drViI5uc3L+mWeIAVoCr9K+Qi5/P2kXA5nkYdcbC10psTdXC3Be9rI16ZYHrpmtcOC30Gvgs4TOzwiV2NSyRfZ3ioX/F02jZuA4W/SIzHW4qFgbqb3S79EIcFSHpBDwWuEHKgWYiEQfMBIHaQI8onnDEET7ysY4Ak3BCq8gT9zuw0faLv5iQEuMe7h5BO7OrJmERupGUoXfTY6HmESiRPpk1NXyU/hfktrkl0y1PF2q990aQBRI5joshRWwJ/DqbyiulzCtT8QAXEJ47bR1OvQ9HgCjY0HItono0+Jn1lEtDntSjtmiqnB7hPyu6ODZ0wt6Pbhj3/e5k7xHHB260syVIhR5kXOA==

Have you tried putting "#[global]" on your hint command, e.g. "#[global] Hint ..."? See the doc at https://coq.github.io/doc/v8.13/refman/proof-engine/vernacular-commands.html#coq:attr.global. Note that some Hint commands don't support this attribute, e.g. "Hint Rewrite".

Hope this helps. Others may know more.

Jim

On Mon, Jan 11, 2021 at 2:23 PM Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

Hi;

I have a Coq proof scripts which is organized in Sections, and I have used Hints inside a section. How do I make sure that these hints are available outside the section?

I also have the same question for Instances.

Also, if someone could point me to examples about managing hints and instances (like Reflexivity, for example. (I am working with some setoids.)) that would be very helpful.

Thank You

--Agnishom

[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