From 3553d5d035f925e6b2f23daad5a8fdd2637a584d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 11 Jun 2018 16:49:27 +0200 Subject: Fix handling of universe context for expanded program obligations. The universe context was dropped even though it isn't added to the global universes yet. Keep it so that it is properly defined with the constant the expanded obligation appears in. --- vernac/obligations.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1ab24b670..e0b1349f7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -865,7 +865,7 @@ let obligation_terminator name num guard hook auto pf = else UState.union prg.prg_ctx ctx in let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in let prg_ctx = @@ -874,10 +874,12 @@ let obligation_terminator name num guard hook auto pf = polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx else - (** The first obligation declares the univs of the constant, + (** The first obligation, if defined, + declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - UState.make (Global.universes ()) + if defined then UState.make (Global.universes ()) + else ctx in let prg = { prg with prg_ctx } in try -- cgit v1.2.3