From e6bffa602c0d744a24d7ea7418020ebd8b7dfbbf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 7 Oct 2017 11:35:34 +0200
Subject: Fix typo in Univ.CumulativityInfo

---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b117f8714b..c2e4d59082 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,7 +234,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
-    let sbsubst = CumulativityInfo.subtyping_susbst cumi in
+    let sbsubst = CumulativityInfo.subtyping_subst cumi in
     let dosubst = subst_univs_level_constr sbsubst in
     let uctx = CumulativityInfo.univ_context cumi in
     let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-- 
cgit v1.2.3