diff options
| author | Hugo Herbelin | 2019-07-27 23:28:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-07-27 23:28:54 +0200 |
| commit | bbec12e3bb2cd1062bd833bbb2c44adbeef33503 (patch) | |
| tree | caf4e355b97c7c1566601aa4c0c4523a7c1aa53f /dev/ci | |
| parent | 2e37b4b30d0779dc960db80189e51ecd69f7e45a (diff) | |
| parent | 75b81316d86b6a76d81b03aef891aeb6df9c814d (diff) | |
Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distr
Reviewed-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: silene
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions