aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-07-26 09:33:55 +0200
committerEmilio Jesus Gallego Arias2018-07-26 09:33:55 +0200
commit6cd6f1edae2e2c7b2aaedd039b39caaf1d50aa9f (patch)
tree684ba0dcb4d13196b80686d8672ba00928ea2fd9 /kernel/nativevalues.ml
parent535f8ce6edea2e2692f5c9c094d3c6fd07411897 (diff)
parente17cbd44317f375e9a281a739facd19e118c1dba (diff)
Merge PR #8150: Fix static declaration of plugins in coqpp.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions