aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/ind_tables.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ind_tables.ml')
-rw-r--r--toplevel/ind_tables.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 5846c73a8..4607e70eb 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -149,7 +149,7 @@ let define_mutual_scheme_base kind suff f internal names mind =
let cl, eff = f mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
- try List.assoc_f Int.equal i names
+ try Int.List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let consts = Array.map2 (define internal) ids cl in
let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in