diff options
author | 2013-10-28 14:08:46 +0100 | |
---|---|---|
committer | 2014-05-06 09:58:54 +0200 | |
commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /toplevel/vernacentries.mli | |
parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'toplevel/vernacentries.mli')
0 files changed, 0 insertions, 0 deletions