diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 14:50:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:21:18 +0100 |
| commit | 58c0784745f8b2ba7523f246c4611d780c9f3f70 (patch) | |
| tree | fb629961a496e4c84491b4e433a9829621179ca6 /checker | |
| parent | 02e6d7f39e3dc2aa8859274bc69b2edf8cc91feb (diff) | |
When declaring constants/inductives use ContextSet if monomorphic.
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 4 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 6 |
3 files changed, 6 insertions, 6 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 354650964..4a0e706aa 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -208,7 +208,7 @@ type constant_def = | OpaqueDef of lazy_constr type constant_universes = - | Monomorphic_const of Univ.universe_context + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which @@ -303,7 +303,7 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 63e28448f..4357a690e 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -29,7 +29,7 @@ let check_constant_declaration env kn cb = (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with - | Monomorphic_const ctx -> push_context ~strict:true ctx env + | Monomorphic_const ctx -> push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in push_context ~strict:false ctx env diff --git a/checker/values.ml b/checker/values.ml index 9e16c8435..5a371164c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli +MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli *) @@ -215,7 +215,7 @@ let v_projbody = let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|] +let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -265,7 +265,7 @@ let v_mind_record = Annot ("mind_record", let v_ind_pack_univs = v_sum "abstract_inductive_universes" 0 - [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|] + [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; |