aboutsummaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/subtyping.ml')
-rw-r--r--kernel/subtyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6354bb0fb6..918a2f51ba 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -331,7 +331,7 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
let mp1 = MPself msid1 in
let env = add_signature mp1 sig1 env in
let sig1 = subst_structure alias sig1 in
- let alias1 = update_subst_alias alias (map_msid msid2 mp1) in
+ let alias1 = update_subst alias (map_msid msid2 mp1) in
let sig2 = subst_structure alias1 sig2' in
let sig2 = subst_signature_msid msid2 mp1 sig2 in
let map1 = make_label_map mp1 sig1 in