aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-27 10:19:21 +0100
committerMaxime Dénès2017-12-27 10:19:21 +0100
commit4969f9425cb0d5cd5bd735110886a0cbd2641588 (patch)
tree6c05276df78dd476642ab5db8437e8730d19eb56 /plugins
parent3921ff2e2c189063ec46f54cbb247570b6c59b2c (diff)
parent5ffa147bd2fe548df3ac9053fe497d0871a5f6df (diff)
Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions