diff options
| author | Brian Campbell | 2020-09-30 17:25:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-09-30 17:26:09 +0100 |
| commit | ce94aec9d6604b41217529525b7a73850c530e7b (patch) | |
| tree | d3311c56f30006e306d13b023e3e03ff39151cd8 /aarch64_small | |
| parent | 36cd0d8a7a146f8d51ef920212be768428680dac (diff) | |
Tweak Coq proof to avoid incompatibility with Iris
(in the previous proof script the intuition tactic found a strange proof
involving a type-level dependent pair that imposed an unnecessary
universe constraint, this doesn't)
Diffstat (limited to 'aarch64_small')
0 files changed, 0 insertions, 0 deletions