diff options
| author | Pierre-Marie Pédrot | 2016-06-17 18:25:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 18:54:43 +0200 |
| commit | 53ced0735f7e24735d78a02fc74588b8d9186eab (patch) | |
| tree | 93661920f42d9be934e59f5f972d165ea24785b7 /kernel/pre_env.ml | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index c307896416..5afefeebde 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -71,6 +71,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; @@ -93,7 +94,8 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = (PredicativeSet,StratifiedType) }; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags; env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -138,6 +140,7 @@ let push_named d env = env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; env_stratification = env.env_stratification; + env_typing_flags = env.env_typing_flags; env_conv_oracle = env.env_conv_oracle; retroknowledge = env.retroknowledge; indirect_pterms = env.indirect_pterms; |