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/values.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 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 46b66adc4..e82ba1032 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -193,7 +193,9 @@ let v_lazy_constr = (** kernel/declarations *) -let v_engagement = v_enum "eng" 1 +let v_impredicative_set = v_enum "impr-set" 2 +let v_type_in_type = v_enum "type-in-type" 2 +let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|] let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -315,7 +317,7 @@ and v_modtype = let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |]) let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|]) let v_compiled_lib = - v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|] + v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|] (** Library objects *) |