Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #173
Closed
Open
Issue created Mar 12, 2018 by Ghost User@ghostContributor

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

Edited Mar 12, 2018 by Ghost User
Assignee
Assign to
Time tracking