Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 12
    • Merge requests 12
  • 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
  • stdpp
  • Merge requests
  • !385

prepare for https://github.com/coq/coq/pull/16289

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Andrej Dudenhefner requested to merge mrhaandi/stdpp:eauto-cost into master Jul 07, 2022
  • Overview 1
  • Commits 1
  • Pipelines 1
  • Changes 1

Due to a bug, eauto neglected the cost of the extern hint lia (and applied it first). However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof. Changing eauto to auto at the specific position would avoid the evar issue.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: eauto-cost