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/topfmt.ml | |
| 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/topfmt.ml')
0 files changed, 0 insertions, 0 deletions