diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index b331d8da7a..c3e59487cb 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -57,6 +57,8 @@ let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context +let opaque_tables env = env.indirect_pterms +let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = match env.env_rel_context, env.env_named_context with |