diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-07 11:35:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-10 01:34:19 +0100 |
| commit | e6bffa602c0d744a24d7ea7418020ebd8b7dfbbf (patch) | |
| tree | b71c3cc2254dd657cb899cc689a834413da27a72 /kernel/indtypes.ml | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
Fix typo in Univ.CumulativityInfo
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 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 |