aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorHugo Herbelin2020-05-11 22:12:47 +0200
committerHugo Herbelin2020-05-11 22:12:47 +0200
commitd640d9debf449dad1f7b1d2eda44a024b78378d1 (patch)
treed20bfee66513b12170541d185caabceb27fce28b /plugins
parent76f7adccc72e6e85bfc2aaec7c5f348e5966b024 (diff)
parent28a698dadd719872a0324a2650172afb12700c01 (diff)
Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlib
Reviewed-by: JasonGross
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions