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: Tue, 12 Jan 2021 10:45:18 -0800
Authentication-results: mail3-smtp-sop.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-f41.google.com
Ironport-phdr: 9a23:Sv7ukxzHbCLu2lvXCy+O+j09IxM/srCxBDY+r6Qd2+gWIJqq85mqBkHD//Il1AaPAdyLraocwLeO++C4ACpcuMnH6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjSu8UMnYduNqk9xxvVrnBVf+ha2X5kKUickhrh5Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyNOAo2+YIUPAeQPPvtWoZfhqFYVtxSyGROhCfnzxjNUhHL727Ax3eQ7EQHB2QwtB9YAsHXRrN7oNKkdT+C1zLPMzTrdcvhb3jX96InNchw7r/GDQ7JwcdDVyUYxDA7FgVCQppbkPzORzOgCr2+b7+95WO+plmUopB1/rCK1yccwlonGmJgVylbc+Chlw4s4O9m1RUF6bNOgEpZcqz+XOYVyT88+X2xlvDo2x7wItJO6YiUH1ogryhrbZvGFfIWG7A/uWumMLDpmmH5ofq+0iRWq8UW41OHwSs253ExJoydFiNXAq3EA2h3J5sWIV/dw+Fqq1yyV2ADJ8O5EJFg5larFJJ4lxb49jp8Tvl7CHi/ygUn2jaiWelg99uim5Onrf6/qppCbN49zhQH+NrohltajDuQ/NwgCR2mb+eKi273/5UD1XqlGg/ksnqTasJ3WP9kXq6+4DgNP3Ysv9g6zDzK839QZmXkHIkhFeBWCj4XxOVHOIfX4Ae2xg1uykDdr3fTGMaP6D5XCK3jMirbhfbJn50FAzwozyMhT54hIBbEZPPLzRkjxucTEAR8+Kgy42vroCNFg1owFQm+PGa+YMKbKsVCS/O4vIu+MZJUUuDnnMfQl6eTu3jcFngoWerDs1p8KYli5GO5nKgOXeynCmNAEREULu0IQQezwjFDKBTxSYjC8UqIm4jwTB4evDIOFTYeo1u/SlBynF4FbMzgVQmuHFm3lIt3dBqU8LRmKK8okqQQqELisT4h7iEOrvQ7+jrtgd6/apnReupXk29x4oebUkENqrG0mP4Gmy2iIClpMsCYNTj4y0rp4pBUkmFiG2Kl8xfdfEI4Kvq8bYkIBLZfZitdCJZXqQAuYJ4WGTV+nRpOtBjRjFt8=

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

"bugs" is taken to include limitations in the common phrase "is that a bug or a feature?". It wouldn't sound as pithy to say "Is that a bug, limitation or 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