aboutsummaryrefslogtreecommitdiff
path: root/kernel/declareops.ml
diff options
context:
space:
mode:
authorClément Pit-Claudel2018-09-24 09:10:47 -0400
committerClément Pit-Claudel2018-09-24 09:10:47 -0400
commitfb8365e96ccb5d25d3810af99c36e7b27fec8fad (patch)
treec516748b678652f998851e13c2f48477a0ca8787 /kernel/declareops.ml
parentc2a1cc7473cf4db27ee47ac011409f7a1839b36d (diff)
parenta454d1dc509aae06eadf7474eb25e90abdf36ca1 (diff)
Merge PR #8541: Update flag, option and table descriptions in coqdomain.py, update README.rst to match.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions