aboutsummaryrefslogtreecommitdiffhomepage
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 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