diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b117f8714..c2e4d5908 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 diff --git a/kernel/univ.ml b/kernel/univ.ml index f72f6f26a..50692ca59 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -968,7 +968,7 @@ struct (univcst, UContext.make (Instance.append inst freshunivs, create_trivial_subtyping inst freshunivs)) - let subtyping_susbst (univcst, subtypcst) = + let subtyping_subst (univcst, subtypcst) = let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' diff --git a/kernel/univ.mli b/kernel/univ.mli index 63bef1b81..975d9045e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -375,7 +375,7 @@ sig trivial subtyping relation. *) val from_universe_context : UContext.t -> Instance.t -> t - val subtyping_susbst : t -> universe_level_subst + val subtyping_subst : t -> universe_level_subst end |