Commits · 4e96f9ee72049c06688b6a9e540a2eff275a159d · Arthur Azevedo de Amorim / stdpp

Jun 19, 2020
- update Makefile · 4e96f9ee
  Ralf Jung authored 4 years ago
  
  4e96f9ee
Jun 18, 2020
- Merge branch 'master' into 'master' · 99bad668
  Robbert Krebbers authored 4 years ago
  
  Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) See merge request !164
  99bad668
- Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi) · 3dce1fea
  sarahzrf authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  3dce1fea
Jun 17, 2020
- Fix compatibility with old Coq versions. · 370c0cf4
  Robbert Krebbers authored 4 years ago
  
  370c0cf4
- Merge branch 'robbert/coq_12512' into 'master' · 2f5854bd
  Robbert Krebbers authored 4 years ago
  
  Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512 See merge request !166
  2f5854bd
Jun 15, 2020
- Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512. · 6af69af1
  Robbert Krebbers authored 4 years ago
  
  6af69af1
- Turn some non-recursive `Fixpoint`s into `Definition`s. · 2ec23bde
  Robbert Krebbers authored 4 years ago
  
  2ec23bde
Jun 14, 2020
- Fix inconsistent space. · 6401d876
  Robbert Krebbers authored 4 years ago
  
  6401d876
May 29, 2020
- Coq 8.11.2 tag exists but there is no such release · 9bd10869
  Ralf Jung authored 4 years ago
  
  9bd10869
- test Coq 8.11.2, and the Coq 8.12 branch · 73e64b7a
  Ralf Jung authored 4 years ago
  
  73e64b7a
- permit building with Coq 8.12 · b6d4c71e
  Ralf Jung authored 4 years ago
  
  b6d4c71e
May 27, 2020
- Merge branch 'fix-forall-scope' into 'master' · 3196e5ca
  Robbert Krebbers authored 4 years ago
  
  Remove type scope from forall notation Closes #67 See merge request !163
  3196e5ca
- Remove type scope from forall notation · b36cd736
  Tej Chajed authored 4 years ago
  
  Fixes #67.
  Verified
  
  b36cd736
- Merge branch 'forall-notation' into 'master' · 60ad150d
  Robbert Krebbers authored 4 years ago
  
  notation for forall See merge request !152
  60ad150d
- notation for forall · bfb8f04e
  Gregory Malecha authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  bfb8f04e
May 12, 2020
- Merge branch 'msammler/rename_Nat2Z_inj_div' into 'master' · ea934fb9
  Robbert Krebbers authored 4 years ago
  
  rename Z2Nat_inj_div and Z2Nat_inj_mod See merge request !161
  ea934fb9
- rename Z2Nat_inj_div and Z2Nat_inj_mod · 0eaae21d
  Michael Sammler authored 4 years ago
  
  0eaae21d
- Merge branch 'revert-a2ac9e66 ' into 'master' · fd5ab7ff
  Robbert Krebbers authored 4 years ago
  
  Revert "Merge branch 'byte-countable' into 'master'" See merge request !160
  fd5ab7ff
- Revert "Merge branch 'byte-countable' into 'master'" · e99804d9
  Robbert Krebbers authored 4 years ago
  
  This reverts merge request !155
  e99804d9
- Merge branch 'byte-countable' into 'master' · a2ac9e66
  Robbert Krebbers authored 4 years ago
  
  Add Countable instances for byte See merge request !155
  a2ac9e66
- Add Countable instances for byte · 5346dd70
  Tej Chajed authored 4 years ago
  
  Verified
  
  5346dd70
- Merge branch 'robbert/list_find' into 'master' · befe38d4
  Robbert Krebbers authored 4 years ago
  
  Lemmas for `list_find` in combination with `app` and `insert`. See merge request iris/stdpp!134
  befe38d4
- CHANGELOG entry. · e6b17ca4
  Robbert Krebbers authored 4 years ago
  
  e6b17ca4
- Lemmas for `list_find` in combination with `app` and `insert`. · 4680e914
  Robbert Krebbers authored 4 years ago
  
  4680e914
- Make `list_find_Some` more `apply` friendly. · 278a845b
  Robbert Krebbers authored 4 years ago
  
  278a845b
- Merge branch 'msammler/rotate' into 'master' · 199c984b
  Robbert Krebbers authored 4 years ago
  
  Rotate everything See merge request iris/stdpp!136
  199c984b
- Added rotate_nat_add, rotate_nat_sub, rotate and rotate_take functions · a613b693
  Michael Sammler authored 4 years ago
  
  a613b693
May 07, 2020
- Merge branch 'ralf/map-forall-lookup' into 'master' · fb90d2d8
  Robbert Krebbers authored 4 years ago
  
  add map_Forall_lookup See merge request iris/stdpp!158
  fb90d2d8
- prove lemma in both directions · a6d4d077
  Ralf Jung authored 4 years ago
  
  a6d4d077
- Merge branch 'bool-leb2' into 'master' · 56a8ce93
  Robbert Krebbers authored 4 years ago
  
  alternative overlay for coq/coq#12162 See merge request iris/stdpp!159
  56a8ce93
- overlay for coq/coq#12162 · 964ea47b
  Olivier Laurent authored 4 years ago
  
  964ea47b
- add map_Forall_lookup · a6f30595
  Ralf Jung authored 4 years ago
  
  a6f30595
May 06, 2020
- Merge branch 'patch-1' into 'master' · 49b8abe5
  Robbert Krebbers authored 4 years ago
  
  tactics.v: Fix parsing precedence for `select` tactic See merge request iris/stdpp!157
  49b8abe5
- tactics.v: Fix parsing precedence for `select` tactic · 6eb05dfc
  Paolo G. Giarrusso authored 4 years ago
  
  Verified
  
  6eb05dfc
May 01, 2020
- Merge branch 'ascii-countable' into 'master' · 432120a3
  Robbert Krebbers authored 4 years ago
  
  Add Countable instance for Ascii.ascii See merge request iris/stdpp!154
  432120a3
Apr 30, 2020
- Add Countable instance for Ascii.ascii · bb75eecc
  Tej Chajed authored 4 years ago
  
  Verified
  
  bb75eecc
Apr 29, 2020
- Avoid overly long line. · 9b75ffdf
  Robbert Krebbers authored 4 years ago
  
  9b75ffdf
Apr 23, 2020
- Merge branch 'msammler/fix_imap_seq0' into 'master' · b9d009d5
  Robbert Krebbers authored 4 years ago
  
  fix imap_seq and imap_seq0 to make them useful See merge request iris/stdpp!151
  b9d009d5
- fix imap_seq and imap_seq0 to make them useful · 94c07daa
  Michael Sammler authored 4 years ago
  
  94c07daa
- Merge branch 'msammler/hintdb_discriminated' into 'master' · 93b578a5
  Robbert Krebbers authored 4 years ago
  
  Create HintDBs with the discriminated option See merge request iris/stdpp!148
  93b578a5