From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: 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. --- interp/declare.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp/declare.ml') 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; }) -- cgit v1.2.3