coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Moving away from putting hints in the core hintdb

From: Armaël Guéneau <armael.gueneau AT ens-lyon.fr>
To: coq-club AT inria.fr, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Subject: Re: [Coq-Club] Moving away from putting hints in the core hintdb
Date: Wed, 14 Nov 2018 21:09:14 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=armael.gueneau AT ens-lyon.fr; spf=Pass smtp.mailfrom=armael.gueneau AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:TBvaBRQ0/hgG6iOSadcV2myiSdpsv+yvbD5Q0YIujvd0So/mwa6yYBCN2/xhgRfzUJnB7Loc0qyK6/+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRcDI2iYYsBD+kPM+hWoIbypVQBsRSwCBKwBO7t0DJEmmP60KM43uknDArI3BYgH9ULsHnMsNj1LqISXvqpy6nM1TrNbu5W3i376IfWaB8hvOyHULVqfsrLzEkgDR3KjlGKpYzqIjOayOINvHaB4Op9Tu+glWgnqxporjirxsYsjY/JipgbylDe7Ch0xps+K96gSENjfNKpH4dcuzuYOoZ0WM8uXmBltSQgxrEYp5K3YjAGxZckyhLFdvCKd5WE7gj+WOuQPzt0nm9pdbG9ihu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL7siIUOBy8Vy/1jqVyQ/T7PpELVkwlavbLJ4hxKQ8lpQJsUjbHy/2nlv5jLOOe0k59eWk9/7rb7fkq5OGKoN5iwPzPr4wlsChH+g0Kg0OUHKa+eS42r3j50r5QLBSg/IsiKnZtYrVKtofpqKjDA9Vz5gs6xChADi8zdQVhmcILFReeB6ei4joO1bOIPbiAfexmVSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjMO6TL9FSM++gHIu+WZYZTtiy5Y9csZOLni0gWmFsXcLO1lc8YYX2kF/IgLESda3f2nv8aEnYRvQs7SeHwzluPTWgASWy1WvcV/DQyi4aRIppCQI2knfTV1T2+F5BSIG9bB1aBGGrAeoOfHvMdbyTULNU3wW9MbqSoV4J0jULmjwT90bcya7OMonRJ56Km78B84qjorT938DV1C8qH1GTUFDN5mHhNQy4x2uZxux4kkwvR4e1Dm/VdUOdrybZRSA5jbszRyfc/D8H1XETPZIXREQv0cpCdGTg0C+kJ7ZoObkJ6QoTwihnJ1SfsDrkO0riaA5py/LiOh3U=

Thanks for the answer!

> Maybe we could add an option "Set Default HintBase mybase", then you
> could use regular option scoping.
>
> ie either put "Set" at the top of every file or module you want it in,
> or "Export Set" in FooOptions.v (where Foo is your project) and import
> that everywhere you want it in.

I think that would be very nice indeed -- maybe generalized to allow
providing a list of default bases? (e.g. Set Default HintBase mybase,
core, arith)

(alternatively, if there was a way to merge databases / import hints
from one in another, it would be enough for the option to take one base;
but there isn't at the moment AFAIK)

[Coq-Club] Moving away from putting hints in the core hintdb, Armaël Guéneau, 11/14/2018
- Re: [Coq-Club] Moving away from putting hints in the core hintdb, Gaëtan Gilbert, 11/14/2018
  - Re: [Coq-Club] Moving away from putting hints in the core hintdb, Armaël Guéneau, 11/14/2018
    - RE: [Coq-Club] Moving away from putting hints in the core hintdb, Jason -Zhong Sheng- Hu, 11/14/2018
      - Re: [Coq-Club] Moving away from putting hints in the core hintdb, Vadim Zaliva, 11/14/2018
        
        Re: [Coq-Club] Moving away from putting hints in the core hintdb, Jacques-Henri Jourdan, 11/15/2018
- RE: [Coq-Club] Moving away from putting hints in the core hintdb, Soegtrop, Michael, 11/15/2018
  - Re: [Coq-Club] Moving away from putting hints in the core hintdb, Jim Fehrle, 11/15/2018
    - RE: [Coq-Club] Moving away from putting hints in the core hintdb, Soegtrop, Michael, 11/16/2018