diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:13:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
| tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /kernel/environ.ml | |
| parent | 591e7e484d544e958595a0fb784336ae050a9c74 (diff) | |
Option -type-in-type: added support in checker and making it contaminating
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a79abbb7e..30b28177c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -46,11 +46,14 @@ let empty_env = empty_env let engagement env = env.env_stratification.env_engagement -let type_in_type env = env.env_stratification.env_type_in_type - let is_impredicative_set env = - match engagement env with - | Some ImpredicativeSet -> true + match fst (engagement env) with + | ImpredicativeSet -> true + | _ -> false + +let type_in_type env = + match snd (engagement env) with + | TypeInType -> true | _ -> false let universes env = env.env_stratification.env_universes @@ -191,11 +194,7 @@ let check_constraints c env = let set_engagement c env = (* Unsafe *) { env with env_stratification = - { env.env_stratification with env_engagement = Some c } } - -let set_type_in_type env = - { env with env_stratification = - { env.env_stratification with env_type_in_type = true } } + { env.env_stratification with env_engagement = c } } let push_constraints_to_env (_,univs) env = add_constraints univs env |