aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.ml')
-rw-r--r--kernel/univ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fd916e77b..7a7e0bb5a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -470,7 +470,7 @@ let is_direct_sort_constraint s v = match s with
let solve_constraints_system levels level_bounds =
let levels =
- Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom"))
+ Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
levels in
let v = Array.copy level_bounds in
let nind = Array.length v in