diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 18:56:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 18:56:49 +0100 |
| commit | af98bb689a05ccf420da53ee7befacb7c2202942 (patch) | |
| tree | 972e28fd5779f101fab9001556010e3986de2c79 /dev/ci | |
| parent | 1b33b57f56f4d53d20318fe9be97dec274086f5b (diff) | |
| parent | 64239322013a30cf25b2a1ca4a8f66bff8a7d818 (diff) | |
Merge PR #11109: Register proof_irrelevance
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions