diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-25 20:44:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 11:26:22 +0100 |
| commit | b58e8aa6525d45473f88fbea71bab88a2b46c825 (patch) | |
| tree | 5900b77b78817d10b45a10f5bd88bb8a0c4059ff /library/universes.ml | |
| parent | 6474fa6c4976c28cd050071df22dd9d87f3cc7b8 (diff) | |
More invariants in UState.
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 = |