diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 054ae17437..fef530c872 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -53,7 +53,6 @@ type env = { 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; } |