diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2018-06-11 16:49:27 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-22 14:18:35 +0200 |
| commit | 3553d5d035f925e6b2f23daad5a8fdd2637a584d (patch) | |
| tree | e5adcd37325d7a652fc6dfced650365f2600295e /vernac | |
| parent | df35025b2be4a0dc9aadecc0e3110a21012683cf (diff) | |
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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/obligations.ml | 8 |
1 files changed, 5 insertions, 3 deletions
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 |