diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-07 11:00:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-07 11:00:46 +0100 |
| commit | 2bb33cd402137f72861eda559c51014f48f6f633 (patch) | |
| tree | 84ce339d612e8a8f648e95727c97e9cc54d70d16 /engine/uState.ml | |
| parent | 9cac9db6446b31294d2413d920db0eaa6dd5d8a6 (diff) | |
| parent | f53156a6d3819682dc888835abcef2b5320dab1b (diff) | |
Merge PR #6290: Rename update to set, Fixes #6196
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 2 |
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 |