Skip to Content.
Sympa Menu

coq-club - [Coq-Club] `Hint Opaque` for `refine`

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] `Hint Opaque` for `refine`


Chronological Thread 
  • From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] `Hint Opaque` for `refine`
  • Date: Wed, 26 Feb 2020 09:00:47 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=Pass smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT ip2.filter01.hostcontrol.com
  • Ironport-phdr: 9a23:MqVUQxdiKHaw2lPXOFgdn2VilGMj4u6mDksu8pMizoh2WeGdxcS8bR7h7PlgxGXEQZ/co6odzbaP7+axAidZuM3JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMSjIZsJao91wbFr3VVcOlK2G1kIk6ekBn76sqs5pBo7j5eu+gm985OUKX6e7o3QLlFBzk4MG47+dPmuwDbQQSA+nUTXGMWkgFVAwfe9xH1Qo3xsirhueVj3iSRIND7Qqo1WTSm6KdrVQPohSIaPDM37G3blsp9h79ArRm/uxJw3ZLbYICNNPp/YKzde88aRXFcVcpVTiBNH5+wY5cKA+cHIO1WrZTyp0EWoBWgBQeiGeDhxDFGiXD5waI03OUhHBra3AEiBd8CrGjYodv3OaoUTOu7zLPIzTLGb/5OxTn975PHfQs/rvGWQbJ7bM/fyVMxGAzelVqft5blPyiI3ekKtmiU9etgVeaui24hpAFxpjmvxtwwionSnY8V0FfE+j5iz4krP924VE17YcS6H5RLrC6VKZF2Qtg4T2FuvCY307sLsoO4cigS0JkqxwTTZ+GHfoWK+B7uV+ecLS13iX9nYL6zmhi//VW6xuHhVcS4zExGojRZntTCrHwBygDf58uBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z74xjpofr17PHiH3mEXykK+ZaF8k9vS15+j9YrXmoYScN5NohQH5NKQuhta/AeM8MgQUQ2eb/uG82KXi/U3/XrpKkuU7n6nDvJzHJckWpLS1DgxU34o55BuyDS+q0NECknkGKFJFdgiHj4/sO1zWJfD3F/a/g1CtkDdtyPDGOrzhAo7RLnjYi7rhZ7F95FVHxwUt19Bf+5FUCqsfL/3oQUD+qsbYDgQjPwyyx+brEM992Z8GWWKTHq+ZN7vfvkOP5uI2OuWDeIsVuCvmJPU+/P7vjXo5mUcHcqWz3JsXbmq4HvV8LEmDb3rsmIRJLWBflQ0nBMfulVfKBTVUfjO5W782zjA9EoOvS4nZENODmruEiR28FJdbfHwOKUqBG33lbZ7MD/IFaSaTJMBlkycYTpC7TIUr2AuytxX3wbBqNPGS/ClO5sGr78R8++CGzUJ6zjdzFcnIljjVFzgpzFNNfCc/2eVEmWI4ylqH1vMg0f1AT5pd5vdVXx1ibNjcyPdmANf0RhjGepGCT1P0Goz6UwF0dco4xpo1W2g4A8+r1EiRxS2gCbIPi7+RCZY+/7jHmX71dZ4kmiT2kZI5hlxjefNhcGivh6px7Q/WXdabiUKTnauwaacG0STH+X2Yi2yK7hhV

Dear all,

There is `Hint Opaque` and `Typeclasses Opaque` to ensure that `auto` and TC search consider certain constants as opaque. Is something similar possible for `(notypeclasses) refine`?

Robbert


  • [Coq-Club] `Hint Opaque` for `refine`, Robbert Krebbers, 02/26/2020

Archive powered by MHonArc 2.6.18.

Top of Page