diff options
author | 2009-02-01 07:30:03 +0100 | |
---|---|---|
committer | 2009-02-01 11:10:05 +0100 | |
commit | 308a600796e061470f233a80b2b7dd71ad766f02 (patch) | |
tree | c7615433423944fa5f101903aa0cb7ae2f42118f /library/decls.ml | |
parent | 10d514272045c3c2551de78c95bcc3175cf29483 (diff) |
Only one out of ledit and cle is needed
Diffstat (limited to 'library/decls.ml')
0 files changed, 0 insertions, 0 deletions