diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index eb5c016922..d95e9fe737 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -139,6 +139,8 @@ let join_safe_environment e = {e with future_cst = []} e.future_cst (* TODO : out of place and maybe incomplete w.r.t. modules *) +(* this is there to explore the opaque pre-env structure but is + * not part of the trusted code base *) let prune_env env = let env = Environ.pre_env env in let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in |