coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon coq

Remove the hint_term type from the Hints API.

Open ppedrot opened this issue 5 months ago • 7 comments

Since we removed the generic constr hint feature, this is now useless.

Overlays:

  • https://github.com/LPCIC/coq-elpi/pull/837
  • https://github.com/mattam82/Coq-Equations/pull/657
  • https://github.com/mit-plv/fiat/pull/123

ppedrot avatar Jun 20 '25 10:06 ppedrot

I'm not sure how to write an overlay for fiat-parsers, the last version defined there is lagging behind (8.19). What's the expected fix? cc @JasonGross

ppedrot avatar Jun 20 '25 13:06 ppedrot

Is there no backwards compatible fix? In any case, I'll update the compact machinery for 8.20, 9.0, 9.1

JasonGross avatar Jun 20 '25 17:06 JasonGross

Oh, sorry, I was thinking this is a different pr. I'll go update the compat machinery

JasonGross avatar Jun 20 '25 17:06 JasonGross

I've updated the infrastructure in https://github.com/mit-plv/fiat/commit/5b11e4b0f8e0e6bd3800f1b8148d59241fee4332, so writing an overlay should now be straightforward

JasonGross avatar Jun 20 '25 18:06 JasonGross

@JasonGross note that we have branched 9.2 already, you should add this version already to fiat-parsers and friends.

ppedrot avatar Jun 20 '25 20:06 ppedrot

Added v9.2 files in https://github.com/mit-plv/fiat/commit/21f4b81eb08ef5d7cebf6794b7adb63e9d05db03

JasonGross avatar Jun 20 '25 23:06 JasonGross

@JasonGross thanks!

ppedrot avatar Jun 21 '25 10:06 ppedrot

@coqbot merge now

SkySkimmer avatar Jun 24 '25 13:06 SkySkimmer

@SkySkimmer: Please take care of the following overlays:

  • 20781-ppedrot-hints-remove-hint-ref.sh

coqbot-app[bot] avatar Jun 24 '25 13:06 coqbot-app[bot]