diff options
author | 2017-12-19 15:37:31 +0100 | |
---|---|---|
committer | 2017-12-19 15:37:31 +0100 | |
commit | ecebaa47890662c2dcb1e6c146a7299f1ed2b1e3 (patch) | |
tree | a55b775ca01ff614f4bb0f9be006ff72a82c2538 /vernac/classes.ml | |
parent | f431dac2e219cb2a76b22e452d6e407869d89f42 (diff) |
Fix warning about shadowing a global name.
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions