Ambiguous reference to eqb in coq_tactics.v
While preparing Coq PR #6948, we noticed a little issue with Bool.eqb
in your development. Indeed, after this PR introducing Ascii.eqb
and String.eqb
in the standard library, your file theories/proofmode/coq_tactics.v
fails to compile due to 2 unqualified references to eqb
not been seen as Bool.eqb
anymore.
This issue can be fixed in a straightforward (and backward-compatible) way : replace the two occurrence of eqb
in this file (lines 95 and 288) by Bool.eqb
(or alternatively, add an Import Bool
at the end of this file's header).
Sorry for not proposing a pull request directly, but apparently I do not have enough permission to fork on your gitlab.
For this fix to be correctly taken in account by our travis testing infrastructure, could you please update the opam
file of repository LambdaRust-coq.git
to mention a fixed version of iris-coq
? Currently it points to iris-coq
version dev.2018-02-23.0
, leading to commit db735a4558ad
.
Thanks! Pierre Letouzey