diff options
| author | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
| commit | 083e83a2e82c17c13b5af7d59029d4ef0aa1b613 (patch) | |
| tree | 7609e9b92c93fe21603aaa2f7d90805e30812f53 /vernac/declareObl.ml | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
| parent | 24a9a9c4bef18133c0b5070992d3396ff7596a7c (diff) | |
Merge PR #9918: Fix #9294: critical bug with template polymorphism
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/declareObl.ml')
| -rw-r--r-- | vernac/declareObl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index e3cffa8523..8fd6bc7eab 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -530,7 +530,7 @@ let obligation_terminator entries uctx { name; num; auto } = declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - if defined then UState.make (Global.universes ()) + if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) else ctx in let prg = {prg with prg_ctx} in |