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 13
    • Merge requests 13
  • 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
  • !343

Avoid unwanted subgoals when applying `from_assumption_exact`

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Maxime Dénès requested to merge maximedenes/iris-coq:fix-from-assumption-exact into master Dec 12, 2019
  • Overview 11
  • Commits 1
  • Pipelines 0
  • Changes 2

Same idea as !342 (closed), but we keep notypeclasses refine, to benefit from the evarconv algorithm. We use shelve explicitly.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: fix-from-assumption-exact