Skip to content
Snippets Groups Projects

Make x.1, x.2 notation compatible with ssrfun.

Merged David Swasey requested to merge swasey/coq-stdpp:ssrfun into master

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.)

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading