Commits · master · Iris / stdpp

28 Jun, 2022 1 commit
- avoid section variables for real · 45fd520d
  Ralf Jung authored Jun 28, 2022
  
  45fd520d
27 Jun, 2022 3 commits
- avoid section variables in printed terms · c4055887
  Ralf Jung authored Jun 27, 2022
  
  c4055887
- adjust regexp · 0a010579
  Ralf Jung authored Jun 27, 2022
  
  0a010579
- normalize away new section variable info · 2b12b6fd
  Ralf Jung authored Jun 26, 2022
  
  2b12b6fd
08 Jun, 2022 1 commit
- ref tests: be less sensitive to trailing spaces · 4f82f462
  Ralf Jung authored Jun 08, 2022
  
  4f82f462
30 May, 2022 6 commits
- Merge branch 'robbert/preimage' into 'master' · 5b7d0bf6
  Robbert Krebbers authored May 30, 2022
```
Preimage function for finite maps.

See merge request !382
```
  5b7d0bf6
- DK → SK. · 28af1927
  Robbert Krebbers authored May 30, 2022
  
  28af1927
- Apply 1 suggestion(s) to 1 file(s) · 58458a53
  Ralf Jung authored May 30, 2022 and Robbert Krebbers committed May 30, 2022
  
  58458a53
- CHANGELOG. · 98723b1c
  Robbert Krebbers authored May 30, 2022
  
  98723b1c
- Rename `lookup_preimage_Some_empty` into `lookup_preimage_Some_non_empty` and add comment. · f64de20e
  Robbert Krebbers authored May 30, 2022
  
  f64de20e
- Add lemma `lookup_total_preimage`. · bb2262ee
  Robbert Krebbers authored May 30, 2022
  
  bb2262ee
25 May, 2022 3 commits
- More curry. · 994462dc
  Robbert Krebbers authored May 25, 2022
  
  994462dc
- Comment. · 13ddd3df
  Robbert Krebbers authored May 25, 2022
  
  13ddd3df
- Preimage function for finite maps. · fc251aa5
  Robbert Krebbers authored May 25, 2022
  
  fc251aa5
16 May, 2022 5 commits
- Merge branch 'janno/cumulative-telescopes' into 'master' · 411eb445
  Ralf Jung authored May 16, 2022
```
Enable cumulativity for telescopes

Closes iris#461

See merge request !380
```
  411eb445
- Move universe-related telescope tests closer together. · b0065fea
  Jan-Oliver Kaiser authored May 16, 2022
  
  b0065fea
- Move `Universe Minimization ToSet` test case higher. · 8eb17fc8
  Jan-Oliver Kaiser authored May 16, 2022
```
The accessor test case also fails when the flag is enabled so that
the dedicated test case for it never has a chance to run.
```
  8eb17fc8
- Enable cumulativity for telescopes. · 6d64bcb5
  Jan-Oliver Kaiser authored May 16, 2022
  
  6d64bcb5
- use flambda for newer Coq · e7d23e65
  Ralf Jung authored May 16, 2022
  
  e7d23e65
13 May, 2022 11 commits
- Merge branch 'robbert/issue_139' into 'master' · 8b17ca72
  Ralf Jung authored May 13, 2022
```
Set `Hint Mode` for `FinSet`.

Closes #139

See merge request !379
```
  8b17ca72
- changelog consistency · 54a2f992
  Ralf Jung authored May 13, 2022
  
  54a2f992
- CHANGELOG. · 51d02793
  Robbert Krebbers authored May 13, 2022
  
  51d02793
- Add test case. · 87779ac4
  Robbert Krebbers authored May 13, 2022
  
  87779ac4
- Set `Hint Mode` for `FinSet`. · 13da2867
  Robbert Krebbers authored May 13, 2022
  
  13da2867
- Merge branch 'robbert/seal' into 'master' · ebb89887
  Robbert Krebbers authored May 13, 2022
```
Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.

See merge request !378
```
  ebb89887
- CHANGELOG. · 458a3fa8
  Robbert Krebbers authored May 13, 2022
  
  458a3fa8
- Hide `_unseal` in results of `Search`. · c215b6cc
  Robbert Krebbers authored May 12, 2022
  
  c215b6cc
- Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`. · 85d5291f
  Robbert Krebbers authored May 12, 2022
  
  85d5291f
- Merge branch 'ralf/dom' into 'master' · 53c9d7f7
  Ralf Jung authored May 13, 2022
```
make dom domain type paremeter (D) implicit

Closes #137

See merge request !376
```
  53c9d7f7
- changelog and FIXME · 6b885cdd
  Ralf Jung authored May 13, 2022
  
  6b885cdd
11 May, 2022 4 commits
- dom: make D type agument name consistent · 3e630f05
  Ralf Jung authored May 09, 2022
  
  3e630f05
- make dom D parameter implicit and adjust Dom Mode · a389ce1b
  Ralf Jung authored May 09, 2022
  
  a389ce1b
- remove Dom instances with alternative domain types · 947d9147
  Ralf Jung authored May 07, 2022
  
  947d9147
- Merge branch 'ralf/drop-8.11' into 'master' · b7a5fed7
  Ralf Jung authored May 11, 2022
```
drop support for Coq 8.11

See merge request !377
```
  b7a5fed7
09 May, 2022 1 commit
- drop support for Coq 8.11 · d9f1c297
  Ralf Jung authored May 09, 2022
  
  d9f1c297
08 May, 2022 1 commit
- normalize OCaml versions · 7c4fd7d6
  Ralf Jung authored May 08, 2022
  
  7c4fd7d6
06 May, 2022 3 commits
- old Coq needs old OCaml · cd39f9a2
  Ralf Jung authored May 06, 2022
  
  cd39f9a2
- looks like there is no 4.13.2 · 3653f955
  Ralf Jung authored May 06, 2022
  
  3653f955
- bump ocaml version · 319a88f6
  Ralf Jung authored May 06, 2022
  
  319a88f6
04 May, 2022 1 commit
- Merge branch 'janno/fix-TargS-notation' into 'master' · 1aceb4c6
  Ralf Jung authored May 04, 2022
```
Annotate telescope notations to support literal telescope arguments.

See merge request !375
```
  1aceb4c6