3 files changed, 4 insertions, 4 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index d57ae89dd..45d2a8b08 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -401,7 +401,7 @@ let rename evk id (evtoid, idtoev) =
   | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
   | Some id' ->
     if Id.Map.mem id idtoev then anomaly (str "Evar name already in use.");
-    (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev))
+    (EvMap.set evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev))
 
 let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
diff --git a/engine/uState.ml b/engine/uState.ml
index 511d55328..c28e78f7d 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -131,7 +131,7 @@ let of_binders b =
 let universe_binders ctx = fst ctx.uctx_names
 
 let instantiate_variable l b v =
-  try v := Univ.LMap.update l (Some b) !v
+  try v := Univ.LMap.set l (Some b) !v
   with Not_found -> assert false
 
 exception UniversesDiffer
diff --git a/engine/universes.ml b/engine/universes.ml
index 93696b4ca..0250295fd 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -491,7 +491,7 @@ module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
 let add_list_map u t map =
   try
     let l = LMap.find u map in
-    LMap.update u (t :: l) map
+    LMap.set u (t :: l) map
   with Not_found ->
     LMap.add u [t] map
 
@@ -584,7 +584,7 @@ let normalize_univ_variable_subst subst =
   let find l = Univ.LMap.find l !subst in
   let update l b =
     assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in
+    try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in
     normalize_univ_variable ~find ~update
 
 let normalize_universe_opt_subst subst =