Do not rely on hints from “ordered_type”

mit-plv / kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

https://plv.csail.mit.edu/kami/

MIT License

142 stars 24 forks source link

Closed vbgl closed 5 years ago

vbgl commented 5 years ago

Some hints from the standard library of Coq will move to a named database; see https://github.com/coq/coq/pull/9772 for details.

This PR changes a few calls to “auto” that implicitly rely on these hints by explicit calls to “discriminate”.

joonwonc commented 5 years ago

Thanks for the change! I've just merged the PR.

vbgl commented 5 years ago

Thanks. Can you also update “bedrock2” to incorporate these changes or should I open a PR there?

Addition: I’ve opened a PR.

joonwonc commented 5 years ago

Many thanks as well to another PR! :)