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.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 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index ede356e69..4ad0327fc 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab val set_opaque_tables : env -> Opaqueproof.opaquetab -> env -val engagement : env -> engagement option +val engagement : env -> engagement val is_impredicative_set : env -> bool - -val type_in_type : env -> bool +val type_in_type : env -> bool (** is the local context empty *) val empty_context : env -> bool @@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env -val set_type_in_type : env -> env - (** {6 Sets of referred section variables } [global_vars_set env c] returns the list of [id]'s occurring either directly as [Var id] in [c] or indirectly as a section variable |