diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 22:08:01 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 22:09:06 +0100 |
commit | edb2b2535d62b37c324c98b28802c1b1699d4014 (patch) | |
tree | 73e2b1964b81b633369cbe06eb08e794f48311a1 /vernac | |
parent | 4940f99922b0784d726b7c50abe63395713f012f (diff) |
Restrict universe context when declaring constants in obligations.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/obligations.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 17a596c42..570f2e5b3 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,13 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in + let typ = nf typ in + let body = nf body in + let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let uctx = UState.restrict prg.prg_ctx uvars in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in - let ubinders = UState.universe_binders prg.prg_ctx in + let ubinders = UState.universe_binders uctx in DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r)) let rec lam_index n t acc = match Constr.kind t with |