Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 121
    • Issues 121
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • 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
  • Iris
  • Issues
  • #336

Closed
Open
Opened Jul 20, 2020 by Tej Chajed@tchajedDeveloper

Use user-supplied names in iIntros (?)

Similar to !479 (merged), the proof mode should preserve user names in binders in iIntros (?).

This depends on !479 (merged) since there's some common infrastructure for representing and threading identifiers through typeclasses.

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#336