From a74c28656a7978c429057b62c34227fe2a6cc432 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 May 2019 19:03:05 +0200 Subject: [Classes] Use prepare_parameter from DeclareDef. This code was originally part of #8811, authored by Gaëtan Gilbert. It seems we are not very consistent on what we do when we use `ParameterEntry`, specially w.r.t. universes but as code cleanup progresses we will have a better view. Co-authored-by: Gaëtan Gilbert --- vernac/comAssumption.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'vernac/comAssumption.ml') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 3406b6276f..27e31f486d 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -173,6 +173,11 @@ let do_assumptions ~pstate ~program_mode kind nl l = uvars, (coe,t,imps)) Univ.LSet.empty l in + (* XXX: Using `DeclareDef.prepare_parameter` here directly is not + possible as we indeed declare several parameters; however, + restrict_universe_context should be called in a centralized place + IMO, thus I think we should adapt `prepare_parameter` to handle + this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in let ubinders = Evd.universe_binders sigma in -- cgit v1.2.3