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 /checker/environ.mli | |
| 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 'checker/environ.mli')
| -rw-r--r-- | checker/environ.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/environ.mli b/checker/environ.mli index 22fe7d8f1..f3b2dd839 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -11,7 +11,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : engagement option; + env_engagement : engagement; } type env = { env_globals : globals; @@ -22,7 +22,7 @@ type env = { val empty_env : env (* Engagement *) -val engagement : env -> Cic.engagement option +val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env (* Digests *) |