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 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • 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
  • Merge requests
  • !512

Fix error when destructing as multiple pats

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Tej Chajed requested to merge tchajed/iris-coq:fix-destruct-multiple-pats into master Sep 24, 2020
  • Overview 3
  • Commits 1
  • Pipelines 0
  • Changes 3

iDestruct H as "H1 H2" produces an error that says the pattern should contain exactly one proper introduction pattern. When multiple patterns are provided, due to Ltac variable shadowing iDestructHypFindPat was instead reporting only the first pattern in the error message (and even that was printed as the parsed AST rather than the original string).

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: fix-destruct-multiple-pats