diff options
| author | Jason Gross | 2017-06-15 18:34:26 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-06-22 21:06:24 -0400 |
| commit | ee8385ef39292fd03bdbae3a7a73726d9fb65e99 (patch) | |
| tree | eaba2ab99aeb3529d7a14310a1fe9906a3b955e1 /API/grammar_API.ml | |
| parent | 8d92701f1a017354504c84d60c9e76da50feaf49 (diff) | |
Put plugin exports in the right compatibility file
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607).
PR #220 put the exports in the wrong compat files, presumably because it
was originally targeted to version 8.6, and this wasn't updated when it
was retargeted to version 8.7.
Diffstat (limited to 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions