Select Git revision
- Branches 20
- master default protected
- ralf/list-module
- msammler/monad_without_universe_constraints
- robbert/new_stuff
- robbert/set_fold_delete
- robbert/rel_decision
- robbert/map_fold_foldr
- robbert/map_Forall_Exist
- robbert/map_disjoint_difference
- ci/refactor_staging
- robbert/cancel_inj_surj
- ralf/make_simple_intropattern
- ralf/lookup_insert
- ralf/multiset-solver
- ralf/empty-opaque
- ralf/listZ
- ralf/hint-mode-plus
- ci-release protected
- ci/msammler/more_feed
- dfrumin/coq-stdpp-set_map_2
- Tags 13
- coq-stdpp-1.11.0 protected
- coq-stdpp-1.10.0 protected
- coq-stdpp-1.9.0 protected
- coq-stdpp-1.8.0 protected
- coq-stdpp-1.7.0 protected
- coq-stdpp-1.6.0 protected
- coq-stdpp-1.5.0 protected
- coq-stdpp-1.4.0 protected
- coq-stdpp-1.3.0 protected
- coq-stdpp-1.2.1 protected
- coq-stdpp-1.2.0 protected
- coq-stdpp-1.1.0 protected
- coq-stdpp-1.0.0 protected
Compare
-
-
- Open in your IDE
- Download source code
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.)
5c069266
History
| Name | Last commit | Last update |
|---|---|---|