diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 16:00:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 16:00:41 +0200 |
| commit | b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (patch) | |
| tree | 1505041402d00c52669f9e430d144c97eae490ff /pretyping/evd.ml | |
| parent | dbdef043ea143f871a3710bae36dfc45fd815835 (diff) | |
Univs: fix bug #3807
Add a flag to disallow minimization to set
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 412fb92b3..3d912ca4c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1324,8 +1324,7 @@ let normalize_evar_universe_context uctx = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic in - if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then - uctx + if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in let uctx' = |