Commits · e7d23e65e3803864f107e72124963bd03e4ce395 · Iris / stdpp

May 16, 2022
- use flambda for newer Coq · e7d23e65
  Ralf Jung authored 2 years ago
  
  e7d23e65
May 13, 2022
- Merge branch 'robbert/issue_139' into 'master' · 8b17ca72
  Ralf Jung authored 2 years ago
  
  Set `Hint Mode` for `FinSet`. Closes #139 See merge request iris/stdpp!379
  8b17ca72
- changelog consistency · 54a2f992
  Ralf Jung authored 2 years ago
  
  54a2f992
- CHANGELOG. · 51d02793
  Robbert Krebbers authored 2 years ago
  
  51d02793
- Add test case. · 87779ac4
  Robbert Krebbers authored 2 years ago
  
  87779ac4
- Set `Hint Mode` for `FinSet`. · 13da2867
  Robbert Krebbers authored 2 years ago
  
  13da2867
- Merge branch 'robbert/seal' into 'master' · ebb89887
  Robbert Krebbers authored 2 years ago
  
  Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. See merge request iris/stdpp!378
  ebb89887
- CHANGELOG. · 458a3fa8
  Robbert Krebbers authored 2 years ago
  
  458a3fa8
- Hide `_unseal` in results of `Search`. · c215b6cc
  Robbert Krebbers authored 2 years ago
  
  c215b6cc
- Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. · 85d5291f
  Robbert Krebbers authored 2 years ago
  
  85d5291f
- Merge branch 'ralf/dom' into 'master' · 53c9d7f7
  Ralf Jung authored 2 years ago
  
  make dom domain type paremeter (D) implicit Closes #137 See merge request iris/stdpp!376
  53c9d7f7
- changelog and FIXME · 6b885cdd
  Ralf Jung authored 2 years ago
  
  6b885cdd
May 11, 2022
- dom: make D type agument name consistent · 3e630f05
  Ralf Jung authored 2 years ago
  
  3e630f05
- make dom D parameter implicit and adjust Dom Mode · a389ce1b
  Ralf Jung authored 2 years ago
  
  a389ce1b
- remove Dom instances with alternative domain types · 947d9147
  Ralf Jung authored 2 years ago
  
  947d9147
- Merge branch 'ralf/drop-8.11' into 'master' · b7a5fed7
  Ralf Jung authored 2 years ago
  
  drop support for Coq 8.11 See merge request iris/stdpp!377
  b7a5fed7
May 09, 2022
- drop support for Coq 8.11 · d9f1c297
  Ralf Jung authored 2 years ago
  
  d9f1c297
May 08, 2022
- normalize OCaml versions · 7c4fd7d6
  Ralf Jung authored 2 years ago
  
  7c4fd7d6
May 06, 2022
- old Coq needs old OCaml · cd39f9a2
  Ralf Jung authored 2 years ago
  
  cd39f9a2
- looks like there is no 4.13.2 · 3653f955
  Ralf Jung authored 2 years ago
  
  3653f955
- bump ocaml version · 319a88f6
  Ralf Jung authored 2 years ago
  
  319a88f6
May 04, 2022
- Merge branch 'janno/fix-TargS-notation' into 'master' · 1aceb4c6
  Ralf Jung authored 2 years ago
  
  Annotate telescope notations to support literal telescope arguments. See merge request !375
  1aceb4c6
May 03, 2022
- Document reasons for using both `exact` and `refine`. · d1bec90c
  Jan-Oliver Kaiser authored 2 years ago
  
  d1bec90c
- Annotate telescope notations to support literal telescope arguments. · 0ab4fb1e
  Jan-Oliver Kaiser authored 2 years ago
  
  0ab4fb1e
Apr 12, 2022
- Merge branch 'robbert/pigeon_hole' into 'master' · 4fb85912
  Robbert Krebbers authored 2 years ago
  
  Add Pigeon Hole principle. See merge request !373
  4fb85912
- CHANGELOG. · 6f9dea44
  Robbert Krebbers authored 2 years ago
  
  6f9dea44
- More pigeonhole. · 8f3ca334
  Robbert Krebbers authored 2 years ago
  
  8f3ca334
- Merge branch 'robbert/tele_arg_ind' into 'master' · f83560b2
  Ralf Jung authored 2 years ago
  
  Add induction principle for `tele_arg`. See merge request !374
  f83560b2
- Show that Pigeon hole principle on nat is a special case of the finite version. · 2b0d874d
  Robbert Krebbers authored 2 years ago
  
  2b0d874d
- Add Pigeon Hole principle. · 296f00b9
  Robbert Krebbers authored 2 years ago
  
  296f00b9
- Add induction principle for `tele_arg`. · 4a3e8ed0
  Robbert Krebbers authored 2 years ago
  
  4a3e8ed0
Apr 11, 2022
- Merge branch 'fixpoint-tele_arg' into 'master' · 045e4d23
  Ralf Jung authored 2 years ago
  
  Define [tele_arg] as a fixpoint See merge request !368
  045e4d23
- tweak changelog · 2635a5e5
  Ralf Jung authored 2 years ago
  
  2635a5e5
- Update the CHANGELOG. · 9d0192a9
  Gregory Malecha authored 2 years ago
  
  9d0192a9
- Use unicode and fix comment. · 835d3d76
  Gregory Malecha authored 2 years ago
  
  835d3d76
- Code formatting. · a0d4deb1
  Gregory Malecha authored 3 years ago
  
  a0d4deb1
- More revisions. · 6f1c3b37
  Gregory Malecha authored 3 years ago
  
  6f1c3b37
- Document the need for [Unset Universe Minimization ToSet]. · 93d78065
  Gregory Malecha authored 3 years ago
  
  93d78065
- Fixup from the review. · b79d6540
  Gregory Malecha authored 3 years ago
  
  b79d6540
- Compatibility with Coq 8.11 (by @Blaisorblade ) · 1812fac1
  Paolo G. Giarrusso authored 3 years ago
  
  1812fac1