diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-17 18:35:03 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-17 18:35:03 +0100 |
commit | 00f82e4411ebbab16fcab99e6c563852a87507a3 (patch) | |
tree | 46aa4acc7d1b9e8d6850c113e73cffbfc7dccb65 /kernel/names.mli | |
parent | 6aa2cd90c3091ebe397d83e1d70caa6237b4b551 (diff) |
Fixing bug #3796.
Diffstat (limited to 'kernel/names.mli')
0 files changed, 0 insertions, 0 deletions