diff options
author | 2017-06-26 21:23:29 +0200 | |
---|---|---|
committer | 2017-06-26 21:23:29 +0200 | |
commit | d7189f0e97dae3f0de9641be3242552873040c44 (patch) | |
tree | 6b926b426a0571f3b228f65a8c94c4c0a7e96c4e /parsing/g_vernac.ml4 | |
parent | 4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (diff) | |
parent | d4a0e0bcc7689457340af5a3007a541b92e12301 (diff) |
Merge PR#826: Put plugin exports in the right compatibility file
Diffstat (limited to 'parsing/g_vernac.ml4')
0 files changed, 0 insertions, 0 deletions