diff options
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/universes.ml b/library/universes.ml index 504a682fc..225e65842 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -650,14 +650,14 @@ let normalize_univ_variable_opt_subst ectx = in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - ectx := Univ.LMap.add l (Some b) !ectx; b + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false in normalize_univ_variable ~find ~update 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); - subst := Univ.LMap.add l b !subst; b in + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = |