search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
718 stars 147 forks source link

Adapt to Coq's PR #18445 fixing inheritance of multiple signatures of implicit arguments in notations #1807

Closed herbelin closed 10 months ago

herbelin commented 10 months ago

With coq/coq#18445, notations hiding constants with multiple signatures of implicit arguments inherit as expected the underlying implicit arguments.

File src/Compilers/Named/ContextProperties/Proper.v was depending on the "bug". We adapt it by changing the notation so that it becomes indifferent to potential insertion of maximal implicit arguments.

Note that this is one possible fix among others (for instance, it is probably also possible to change the signatures of the underlying constant).

It is (a priori) backwards compatible and can be merged as soon as now.

JasonGross commented 10 months ago

Thank you!