diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-08 19:28:20 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-08 19:28:20 +0000 |
commit | 82f8e76c38f7d5904ee78bfed3cfddb87efa9f92 (patch) | |
tree | b617ffbd4202e2a1e35deee28db76ff8db6a1704 /parsing/extrawit.ml | |
parent | a7073580104d2e51ffb446b133b5846d9f14e49e (diff) |
Extraction: restrict autoinling to csts whose body is globally visible (fix #2241)
Here, the constants "without body" we don't want to autoinline are
constants made opaque by the rigid signature of their module.
As mentionned by X.L. inlining them might lead to untypable code.
The current solution is safe, but not ideal: we could want to inline
such constants at least inside their own module, and we could also
want to inline constants that are not globally visible (functors...).
NB: AutoInline is anyway not activated by default anymore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/extrawit.ml')
0 files changed, 0 insertions, 0 deletions