The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Hi,

Global/global is not supported by the Hint commands in sections as indicated in https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#creating-hints so you have no choice but to redeclare the hints after closing a section. However, it is supported for the Instance command.

Théo

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

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