Skip to content

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

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