Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
S
stdpp
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 54
    • Issues 54
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 7
    • Merge Requests 7
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge Requests
  • !54

Merged
Created Feb 07, 2019 by Robbert Krebbers@robbertkrebbersMaintainer

Seal `fresh_generic`.

  • Overview 2
  • Commits 1
  • Changes 1

Since fresh_generic is too inefficient for all practical purposes, we seal off its definition. That way, Coq will not accidentally unfold it during unification or other tactics.

This issue actually occurred in iGPS, as reported by Hai.

Edited Feb 07, 2019 by Robbert Krebbers
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Source branch: robbert/seal_fresh_generic