From b58e8aa6525d45473f88fbea71bab88a2b46c825 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 25 Nov 2015 20:44:08 +0100
Subject: More invariants in UState.

---
 library/universes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/universes.ml b/library/universes.ml
index 504a682fc2..225e658425 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 =
-- 
cgit v1.2.3