diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:59:24 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:59:24 +0200 |
| commit | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (patch) | |
| tree | 73222697d2a80aa2ac34d46eb83f1172504e4cc9 /vernac | |
| parent | f6fe2741610552ffc9eb8cbe1f9061dedf965f90 (diff) | |
| parent | 3553d5d035f925e6b2f23daad5a8fdd2637a584d (diff) | |
Merge PR #7775: Fix handling of universe context for expanded program obligations.
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 |