aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..aa14f66df6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
let declarenew g =
LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
in
- let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+ let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
uctx_local = local;
uctx_seff_univs = seff;