aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-03-26 23:00:05 +0100
committerGaëtan Gilbert2019-03-26 23:00:05 +0100
commit2c37c0e7eea9b8406e534e93881158bb6919ed38 (patch)
tree0dac1382c8d44eecb31e3390beb5b1ece1704263 /kernel/nativevalues.ml
parente8fd832d9e487fa57e2efe627223d04ff2977fa9 (diff)
Incorrect details in critical bug info (prop_set_proof_irrelevance)
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions