Commits · master · Alix Trieu / stdpp

10 Jul, 2020 2 commits
- Merge branch 'clarify-which-bsd' into 'master' · 0a92e2be
  Robbert Krebbers authored Jul 10, 2020
```
LICENSE: Clarify which BSD license is being used

See merge request iris/stdpp!174
```
  0a92e2be
- LICENSE: Clarify which BSD license is being used · d6ab6561
  Paolo G. Giarrusso authored Jul 10, 2020
```
Sister MR to iris!472.
```
  d6ab6561
02 Jul, 2020 4 commits
- Merge branch 'doc-gmap-reduction' into 'master' · c8129a37
  Robbert Krebbers authored Jul 02, 2020
```
Sketch docs for computation on [gmap], since they're a FAQ

See merge request iris/stdpp!171
```
  c8129a37
- Add docs for computation on [gmap], since they're a FAQ · 8517b23b
  Paolo G. Giarrusso authored Jul 02, 2020
```
Also, document why [simpl never] is not enough, with a link to an alternative
design.
```
  8517b23b
- Merge branch 'ralf/drop-8.7' into 'master' · 04d69616
  Robbert Krebbers authored Jul 02, 2020
```
drop support for Coq 8.7

See merge request iris/stdpp!170
```
  04d69616
- drop support for Coq 8.7 · 852e6fa7
  Ralf Jung authored Jul 02, 2020
  
  852e6fa7
29 Jun, 2020 1 commit
- Merge branch 'robbert/multiset_solver' into 'master' · 376e5e05
  Robbert Krebbers authored Jun 29, 2020
```
Add solver `multiset_solver` for multisets

See merge request iris/stdpp!167
```
  376e5e05
25 Jun, 2020 5 commits
- Make `multiset_solver` stronger by also considering `multiplicity` in hyps. · 45b64e21
  Robbert Krebbers authored Jun 25, 2020
  
  45b64e21
- CHANGELOG. · f4269240
  Robbert Krebbers authored Jun 25, 2020
  
  f4269240
- Add tests for `multiset_solver`. · 8f80353d
  Robbert Krebbers authored Jun 25, 2020
  
  8f80353d
- Add solver `multiset_solver` for multisets. · d3d95ed9
  Robbert Krebbers authored Jun 25, 2020
  
  d3d95ed9
- Export `Countable` in `gmultiset`, without that, the file is useless. · fd6905fa
  Robbert Krebbers authored Jun 25, 2020
  
  fd6905fa
23 Jun, 2020 1 commit
- Merge branch 'gset-gmap-delete' into 'master' · 6ee0e09e
  Robbert Krebbers authored Jun 23, 2020
```
Prove theorem about delete of gset_to_gmap

See merge request iris/stdpp!162
```
  6ee0e09e
19 Jun, 2020 2 commits
- bump Coq to 8.11.2 · aa5e294c
  Ralf Jung authored Jun 19, 2020
  
  aa5e294c
- update Makefile · 4e96f9ee
  Ralf Jung authored Jun 19, 2020
  
  4e96f9ee
18 Jun, 2020 2 commits
- Merge branch 'master' into 'master' · 99bad668
  Robbert Krebbers authored Jun 18, 2020
```
Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

See merge request iris/stdpp!164
```
  99bad668
- Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) · 3dce1fea
  sarahzrf authored Jun 18, 2020 and Robbert Krebbers committed Jun 18, 2020
  
  3dce1fea
17 Jun, 2020 2 commits
- Fix compatibility with old Coq versions. · 370c0cf4
  Robbert Krebbers authored Jun 17, 2020
  
  370c0cf4
- Merge branch 'robbert/coq_12512' into 'master' · 2f5854bd
  Robbert Krebbers authored Jun 17, 2020
```
Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

See merge request iris/stdpp!166
```
  2f5854bd
15 Jun, 2020 2 commits
- Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512. · 6af69af1
  Robbert Krebbers authored Jun 15, 2020
  
  6af69af1
- Turn some non-recursive `Fixpoint`s into `Definition`s. · 2ec23bde
  Robbert Krebbers authored Jun 15, 2020
  
  2ec23bde
14 Jun, 2020 1 commit
- Fix inconsistent space. · 6401d876
  Robbert Krebbers authored Jun 14, 2020
  
  6401d876
29 May, 2020 3 commits
- Coq 8.11.2 tag exists but there is no such release · 9bd10869
  Ralf Jung authored May 29, 2020
  
  9bd10869
- test Coq 8.11.2, and the Coq 8.12 branch · 73e64b7a
  Ralf Jung authored May 29, 2020
  
  73e64b7a
- permit building with Coq 8.12 · b6d4c71e
  Ralf Jung authored May 29, 2020
  
  b6d4c71e
27 May, 2020 4 commits
- Merge branch 'fix-forall-scope' into 'master' · 3196e5ca
  Robbert Krebbers authored May 28, 2020
```
Remove type scope from forall notation

Closes #67

See merge request iris/stdpp!163
```
  3196e5ca
- Remove type scope from forall notation · b36cd736
  Tej Chajed authored May 27, 2020
```
Fixes #67.
```
  b36cd736
- Merge branch 'forall-notation' into 'master' · 60ad150d
  Robbert Krebbers authored May 27, 2020
```
notation for forall

See merge request iris/stdpp!152
```
  60ad150d
- notation for forall · bfb8f04e
  Gregory Malecha authored May 27, 2020 and Robbert Krebbers committed May 27, 2020
  
  bfb8f04e
26 May, 2020 1 commit
- Prove theorem about delete of gset_to_gmap · a04b0a88
  Tej Chajed authored May 26, 2020
  
  a04b0a88
12 May, 2020 10 commits
- Merge branch 'msammler/rename_Nat2Z_inj_div' into 'master' · ea934fb9
  Robbert Krebbers authored May 12, 2020
```
rename Z2Nat_inj_div and Z2Nat_inj_mod

See merge request iris/stdpp!161
```
  ea934fb9
- rename Z2Nat_inj_div and Z2Nat_inj_mod · 0eaae21d
  Michael Sammler authored May 12, 2020
  
  0eaae21d
- Merge branch 'revert-a2ac9e66' into 'master' · fd5ab7ff
  Robbert Krebbers authored May 12, 2020
```
Revert "Merge branch 'byte-countable' into 'master'"

See merge request iris/stdpp!160
```
  fd5ab7ff
- Revert "Merge branch 'byte-countable' into 'master'" · e99804d9
  Robbert Krebbers authored May 12, 2020
```
This reverts merge request !155
```
  e99804d9
- Merge branch 'byte-countable' into 'master' · a2ac9e66
  Robbert Krebbers authored May 12, 2020
```
Add Countable instances for byte

See merge request iris/stdpp!155
```
  a2ac9e66
- Add Countable instances for byte · 5346dd70
  Tej Chajed authored May 01, 2020
  
  5346dd70
- Merge branch 'robbert/list_find' into 'master' · befe38d4
  Robbert Krebbers authored May 12, 2020
```
Lemmas for `list_find` in combination with `app` and `insert`.

See merge request iris/stdpp!134
```
  befe38d4
- CHANGELOG entry. · e6b17ca4
  Robbert Krebbers authored May 12, 2020
  
  e6b17ca4
- Lemmas for `list_find` in combination with `app` and `insert`. · 4680e914
  Robbert Krebbers authored Mar 31, 2020
  
  4680e914
- Make `list_find_Some` more `apply` friendly. · 278a845b
  Robbert Krebbers authored Mar 31, 2020
  
  278a845b