aboutsummaryrefslogtreecommitdiff
path: root/kernel/declareops.ml
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-08-06 23:34:07 +0200
committerErik Martin-Dorel2019-08-08 11:11:54 +0200
commitd4e07328f7aed9d19e9b9a0f442e8fe85643073a (patch)
tree126508ec26b3cd4fd4072fd689ed5366596c3a4c /kernel/declareops.ml
parent05ae4be1258ed198949f886e83151fb41f7dedb1 (diff)
[doc][ssr][under][setoid] Add changelog entry
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions