diff options
| author | Pierre Roux | 2019-11-13 11:34:15 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-13 13:28:18 +0100 |
| commit | 64239322013a30cf25b2a1ca4a8f66bff8a7d818 (patch) | |
| tree | 1c5beec05de5a10296ea729c3859a5de42d79d94 /dev | |
| parent | c45f079c52524da687dfcc9e5f5511d6e86bc537 (diff) | |
Register proof_irrelevance
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions