diff options
| author | Gaëtan Gilbert | 2019-05-21 12:43:50 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-21 12:43:50 +0200 |
| commit | 02d6f5660d54fcf4dfc9cff36cbda41dca3f601f (patch) | |
| tree | d3ab4306b1220e1e9477c459dbbff22990833ccb /vernac/comAssumption.ml | |
| parent | afb1a427debbc32aef1b2df0b31aa9cf8938b687 (diff) | |
| parent | a74c28656a7978c429057b62c34227fe2a6cc432 (diff) | |
Merge PR #10042: [Classes] Use prepare_parameter from DeclareDef.
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |