diff options
| -rw-r--r-- | toplevel/obligations.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index e8682c1b5..b942034df 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -796,9 +796,9 @@ let solve_by_tac name evi t poly ctx = let entry = Term_typing.handle_entry_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); - assert(Univ.ContextSet.is_empty (snd body)); + let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, ctx' + (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in |