Merge branch 'v8.5'

1 files changed, 4 insertions, 1 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 574be9844a..cd0b52ecaa 100644
--- a/engine/evd.ml
+++ b/engine/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;