diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 10c9c27cb5..f634719f9a 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -46,6 +46,7 @@ type env = { env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; + env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge } type named_context_val = named_context * named_vals |