diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-04 14:50:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-06 10:01:19 +0200 |
| commit | 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f (patch) | |
| tree | 4bb7a90d8474b038434b732fb24b9b9d69e937c3 /pretyping/evd.ml | |
| parent | efce61af32ff1b09a21dcf88bca7d6609a0bfd27 (diff) | |
Fix bug #4354: interpret hints in the right env and sigma.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 842b87c57..4e0b6f75e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -312,7 +312,10 @@ let union_evar_universe_context ctx ctx' = let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in - let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in + let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let declarenew g = + Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g + in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; |