diff options
| author | letouzey | 2009-12-08 12:44:20 +0000 |
|---|---|---|
| committer | letouzey | 2009-12-08 12:44:20 +0000 |
| commit | 82b68be9cf697a60ca393f99096fc7cbbf3379db (patch) | |
| tree | 17461ef4d92340d2b2be9763a1f6dfd5328103e4 /dev/include | |
| parent | f468e43f60f433f0f3f60d394d617072d0aed143 (diff) | |
Sos.ml: no more warnings
apart for a few non-exhaustive patterns, there was also some unused
let-in variables. Hard to check whether the apparently useless code
is doing some side-effect or not... It seems not, so I've removed
completely the corresponding code. Frederic, is that ok ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12570 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions