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

0 files changed, 0 insertions, 0 deletions