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 353c46112..e551d22c8 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -50,6 +50,7 @@ type env = { env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; + env_typing_flags : typing_flags; env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; |