diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-24 15:19:46 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:11 +0200 |
| commit | 6902d2bcb2840619d4c6f41a0d30948daa877b0c (patch) | |
| tree | 44abfa32f386f7b3dc7cc62a234819bd1c115832 | |
| parent | e86b5cf5beab9a67c65afa7456feb417df9d465c (diff) | |
Univs/program: handle side effects in obligations.
| -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 |