theories/base.v · 5c069266f5f2fa9212575d036385aeaec7622069 · Glen Mével / stdpp

Forked from Iris / stdpp

Source project has a limited visibility.

7 years ago

Make x.1, x.2 notation compatible with ssrfun. · 5c069266

David Swasey authored 7 years ago

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

History

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

David Swasey authored 7 years ago

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