diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-11-24 15:48:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-11-24 15:50:32 +0100 |
| commit | 2d32a2c5606286c85fd35c7ace167b4d4e108ced (patch) | |
| tree | 43dd55e9ff642f92ad045864126f64e24a2436af /toplevel/obligations.ml | |
| parent | 1467c22548453cd07ceba0029e37c8bbdfd039ea (diff) | |
Univs: carry on universe substitution when defining obligations of
non-polymorphic definitions, original universes might be substituted
later on due to constraints.
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 311c61f89..e091d825c 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -823,7 +823,9 @@ let obligation_hook prg obl num auto ctx' _ gr = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - Evd.evar_universe_context (Evd.from_env (Global.env ())) + let evd = Evd.from_env (Global.env ()) in + let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in + Evd.evar_universe_context ctx' else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -899,8 +901,10 @@ and solve_obligation_by_tac prg obls i tac = let def, obl' = declare_obligation !prg obl t ty uctx in obls.(i) <- obl'; if def && not (pi2 !prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in prg := {!prg with prg_ctx = ctx'}); true else false |