diff options
| author | Matthieu Sozeau | 2015-10-07 16:00:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-07 16:02:34 +0200 |
| commit | 08a0c44e3525d1f0c7303d189e826e25c3e3d914 (patch) | |
| tree | b839cda5ae1746bfe90f51b609909fb76f981820 | |
| parent | 27492a7674587e1a3372cd7545e056e2775c69b3 (diff) | |
Univs: fix FingerTree contrib.
Let merge_context_set be lenient when merging the context of side
effects of an entry from solve_by_tac.
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4372668fcf..412fb92b3d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1028,8 +1028,8 @@ let merge_uctx sideff rigid uctx ctx' = let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } -let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx false rigid evd.universes ctx'} +let merge_context_set ?(sideff=false) rigid evd ctx' = + {evd with universes = merge_uctx sideff rigid evd.universes ctx'} let merge_uctx_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 5a59c1776c..52d7d42120 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -542,7 +542,7 @@ val universes : evar_map -> Univ.universes val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b942034df7..00ea2ffb84 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -796,7 +796,7 @@ 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); - let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + let ctx' = Evd.merge_context_set ~sideff:true 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, Evd.evar_universe_context ctx' |