aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/plugin_base.dune
diff options
context:
space:
mode:
authorMatthieu Sozeau2018-11-27 11:20:57 +0100
committerMatthieu Sozeau2018-11-27 11:20:57 +0100
commitf6a2d21b6c2a93cb70fde235fc897fb75ea51384 (patch)
tree8913811d7ff06686a0ec837296545cae12007f85 /plugins/syntax/plugin_base.dune
parentdddb72b2f45f39f04e91aa9099bcd1064c629504 (diff)
parentc58ea20fba5a5ce54aaf62182dfd3ee8a368d529 (diff)
Merge PR #8850: Private universes for opaque polymorphic constants.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions