diff options
| author | Gaëtan Gilbert | 2017-10-07 11:35:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-10 01:34:19 +0100 |
| commit | e6bffa602c0d744a24d7ea7418020ebd8b7dfbbf (patch) | |
| tree | b71c3cc2254dd657cb899cc689a834413da27a72 /kernel | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
Fix typo in Univ.CumulativityInfo
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 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 diff --git a/kernel/univ.ml b/kernel/univ.ml index f72f6f26a9..50692ca590 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 63bef1b81b..975d9045ee 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 |