diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /kernel/environ.ml | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
Add a non-cumulative impredicative universe SProp.
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ab046f02f7..5f6d5f3d0e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -59,7 +59,8 @@ type globals = { type stratification = { env_universes : UGraph.t; - env_engagement : engagement + env_engagement : engagement; + env_sprop_allowed : bool; } type val_kind = @@ -117,7 +118,9 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet }; + env_engagement = PredicativeSet; + env_sprop_allowed = false; + }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -243,7 +246,7 @@ let is_impredicative_set env = | _ -> false let is_impredicative_sort env = function - | Sorts.Prop -> true + | Sorts.SProp | Sorts.Prop -> true | Sorts.Set -> is_impredicative_set env | Sorts.Type _ -> false @@ -432,6 +435,14 @@ let set_typing_flags c env = (* Unsafe *) if same_flags env.env_typing_flags c then env else { env with env_typing_flags = c } +let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative + +let set_allow_sprop b env = + { env with env_stratification = + { env.env_stratification with env_sprop_allowed = b } } + +let sprop_allowed env = env.env_stratification.env_sprop_allowed + (* Global constants *) let no_link_info = NotLinked |