diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 16:00:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 16:02:34 +0200 |
| commit | 08a0c44e3525d1f0c7303d189e826e25c3e3d914 (patch) | |
| tree | b839cda5ae1746bfe90f51b609909fb76f981820 /pretyping/evd.ml | |
| 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.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4372668fc..412fb92b3 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 } |