diff options
| author | letouzey | 2013-09-19 17:37:21 +0000 |
|---|---|---|
| committer | letouzey | 2013-09-19 17:37:21 +0000 |
| commit | efae3184752f19a6cfb95b05ad42438c87ee3a9e (patch) | |
| tree | 055e4e67f22badc405252b7f84894ff63d1ce054 /kernel/nativecode.mli | |
| parent | 736ffcea3a04da40ea3047216864ca420f220fe5 (diff) | |
Prettyp: avoid useless "let module"
As hinted by X. Clerc, a "let module" induces some runtime cost,
so let's try to avoid them when possible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions