- Feb 03, 2018
-
-
Ralf Jung authored
-
- Feb 02, 2018
-
-
Robbert Krebbers authored
-
- Jan 31, 2018
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jan 25, 2018
- Jan 23, 2018
-
-
Ralf Jung authored
-
- Jan 14, 2018
-
-
Robbert Krebbers authored
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.
-
- Jan 13, 2018
-
-
Robbert Krebbers authored
Add a Notation for `sn`: strongly normalizing. See merge request robbertkrebbers/coq-stdpp!25
-
- Jan 12, 2018
-
-
Robbert Krebbers authored
-
- Jan 10, 2018
-
-
Robbert Krebbers authored
As we have for all classes for binary relations.
-
- Dec 19, 2017
-
-
Ralf Jung authored
-
- Dec 18, 2017
- Dec 17, 2017
- Dec 08, 2017
-
-
Robbert Krebbers authored
-
- Dec 05, 2017
-
-
Robbert Krebbers authored
typeclass comments See merge request robbertkrebbers/coq-stdpp!24
-
Ralf Jung authored
-
- Dec 04, 2017
-
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
Lattices notation for order, join, meet, top and bot. See merge request robbertkrebbers/coq-stdpp!23
-
Jacques-Henri Jourdan authored
-
- Nov 29, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Make x.1, x.2 notation compatible with ssrfun. See merge request robbertkrebbers/coq-stdpp!21
-
David Swasey authored
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.)
-
