diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 19:36:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 19:36:49 +0000 |
| commit | ebaecfe6c1e84fa3615b295dad85cbf4318a4c75 (patch) | |
| tree | 8f44e08e2f5de6dd8d92f94dd90e1eea29ace627 /library/declaremods.mli | |
| parent | d3097cd34ffffda5dbe332ee88fd33d54180fad9 (diff) | |
Declaremods: drop some useless stuff (slight gain in vo size)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16406 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
0 files changed, 0 insertions, 0 deletions