diff options
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index c5254b453..4ef89f8c0 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -75,7 +75,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; } @@ -98,8 +97,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags; - env_conv_oracle = Conv_oracle.empty; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } |