coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] How do I make Hints available outside a section?
Date: Mon, 11 Jan 2021 16:23:14 -0600
Authentication-results: mail2-smtp-roc.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:ZzyupxA2/fcLmI8LmLhcUyQJP3N1i/DPJgcQr6AfoPdwSPT5ocbcNUDSrc9gkEXOFd2Cra4d1KyM7vmrADFRqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswncttQajYR/JqsxzhbCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCM//WrKiMJ/kbhbrQquqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv0cDrRS4BQmtH+PvyjhIhnrr1qAk0+QuCx3G3BAnH9IWqnvbsdX1NacIXuG10aLFyi/Mb/xQ2Tf884jIchchofSXUL1sdMrRyFMjGBnZgVmKqIzlOSqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hhIfXio4IxV3J6Tl1zokrKNGlR0B2bsKoHZ9QuiyaKYd7X90uT310tSs+xLMLu5C2cTQJxZkk2hLSav6KfoaM7x/lSe2fIi94iWp4dL6hiRu+60mtx+PmWsWqzFpHoDBJnsfRunwTzxDf9NSLR/9n8kqi2TuDzR3f5+BFLEwumqfWK5gsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl6+H9bbXnop+QLZN7igT/Mqg0gMOwHf40MgkIX2SD+OS80qPs/VHhTblXkPE7nLPVvZHUKMgBuKK1HwFY3pw95xqiETuqyNEYkmMGLFJBdhKHlY/pO1TWLf/iAve/hVWskCxrx/DBO73sGYnCLn3CkLv7Z7ly91RQyAs1zdxH/ZJbFqkBIO7vWk/2rNHXEhg5MxWtz+n7DNV9y5gRVHmUAq6ZNaPSqUWH6vguI+mKfo8VuSzyJ+Ir5/703jcFngoWerDs1p8KYli5GO5nKgOXeynCmNAERE4FuAslTOvvwHaCWCJPYG67U6It7yBzXIupC4bYRoeoqLeE3WGyFdtXYDYVWRi3DX70etDcCL83YyWIL5o5y2BWZf2aU4YkkCqWmkri0bM+d7jf/yxevJml1d4nv7SCxyF3ziR9CoGm60/ISmh1mm0SQDpvhfJ0pE07w1zF0K4q2qUFR+wW3OtAV0IBDbCZz+F+DImsCAfIf9PPQ1OnBNytRzA3HIo8

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