Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 22
    • Merge requests 22
  • 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
  • #216
Closed
Open
Issue created Oct 14, 2018 by Robbert Krebbers@robbertkrebbersMaintainer

Replace most occurences of `.. || ..` by `first [..|..]`

Today I found out, as described in the Coq documentation, that the behavior of e1 || e2 in Ltac is not what I expected. It will execute e2 not just when e1 fails, but also when it does not make any progress.

This problem came up when debugging an issue reported by YoungJu Song on Mattermost. He noticed that the wp_bind tactic does not work when one tries to bind the top-level term. The code of wp_bind contains:

reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
|| fail "wp_bind: cannot find" efoc "in" e

wp_bind_core is special casing the context [], and then performs just an idtac instead of actually using the bind rule for WP.

Assignee
Assign to
Time tracking