Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • C coq-stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • David Swasey
  • coq-stdpp
  • Repository
Switch branch/tag
  • coq-stdpp
  • theories
  • base.v
Find file BlameHistoryPermalink
  • David Swasey's avatar
    Make x.1, x.2 notation compatible with ssrfun. · 5c069266
    David Swasey authored Nov 29, 2017
    Enable one to import both stdpp's base and ssrfun.
    
    Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
    (This change affects one proof in Iris.)
    5c069266