diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-10-02 19:23:51 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-10-02 19:23:51 +0200 |
| commit | b7374d225af55ecc6f5d6aa8f3684bfae99ff465 (patch) | |
| tree | 75a9858d151984c2033c66fa171bed3305fa20ce /exportclight | |
| parent | ca5f8a7629a6e31cc287139ad0a69b8154514260 (diff) | |
| download | compcert-kvx-b7374d225af55ecc6f5d6aa8f3684bfae99ff465.tar.gz compcert-kvx-b7374d225af55ecc6f5d6aa8f3684bfae99ff465.zip | |
Make explicit the use of hints from OrderedType (#316)
Some hints will move from the core database to the `ordered_type` database
(see https://github.com/coq/coq/pull/9772).
This commit prepares for this move by adding `with ordered_type` to the invocations
of `auto` and `eauto` that use the hints in question.
Diffstat (limited to 'exportclight')
0 files changed, 0 insertions, 0 deletions