diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /kernel/environ.ml | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index ab046f02f7..97c9f8654a 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 @@ -537,7 +548,7 @@ let lookup_projection p env = match mib.mind_record with | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection") | PrimRecord infos -> - let _,_,typs = infos.(i) in + let _,_,_,typs = infos.(i) in typs.(Projection.arg p) let get_projection env ind ~proj_arg = |