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 /interp/declare.ml | |
| 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 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index dc77981f2..15999f1d1 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -207,7 +207,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = let univs = if poly then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + else + (* FIXME be smarter about this *) + Monomorphic_const_entry (Univ.ContextSet.of_context univs) in { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; @@ -340,7 +342,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; }) |