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