summaryrefslogtreecommitdiff
path: root/lib/coverage
diff options
context:
space:
mode:
authorBrian Campbell2020-09-30 17:25:56 +0100
committerBrian Campbell2020-09-30 17:26:09 +0100
commitce94aec9d6604b41217529525b7a73850c530e7b (patch)
treed3311c56f30006e306d13b023e3e03ff39151cd8 /lib/coverage
parent36cd0d8a7a146f8d51ef920212be768428680dac (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 'lib/coverage')
0 files changed, 0 insertions, 0 deletions