diff options
| -rw-r--r-- | checker/indtypes.ml | 6 | ||||
| -rw-r--r-- | checker/univ.ml | 19 | ||||
| -rw-r--r-- | checker/univ.mli | 4 |
3 files changed, 5 insertions, 24 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 00ff447cc..69dd6f57a 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -551,10 +551,10 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con let check_subtyping mib paramsctxt env_ar inds = let numparams = rel_context_nhyps paramsctxt in let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in - let dosubst = subst_univs_level_constr sbsubst in + let dosubst = subst_instance_constr sbsubst in let uctx = Univ.UInfoInd.univ_context mib.mind_universes in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env' = Environ.push_context uctx env_ar in let env'' = Environ.push_context uctx_other env' in diff --git a/checker/univ.ml b/checker/univ.ml index fa884d9d0..525f535e9 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1194,8 +1194,7 @@ struct create_trivial_subtyping inst freshunivs)) let subtyping_susbst (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' + let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx' end @@ -1232,22 +1231,6 @@ let subst_univs_level_universe subst u = if u == u' then u else Universe.sort u' -let subst_univs_level_instance subst i = - let i' = Instance.subst_fn (subst_univs_level_level subst) i in - if i == i' then i - else i' - -let subst_univs_level_constraint subst (u,d,v) = - let u' = subst_univs_level_level subst u - and v' = subst_univs_level_level subst v in - if d != Lt && Level.equal u' v' then None - else Some (u',d,v') - -let subst_univs_level_constraints subst csts = - Constraint.fold - (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) - csts Constraint.empty - (** Substitute instance inst for ctx in csts *) let subst_instance_level s l = diff --git a/checker/univ.mli b/checker/univ.mli index edf828dae..2bc2653e0 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -213,7 +213,7 @@ sig val from_universe_context : universe_context -> universe_instance -> t - val subtyping_susbst : t -> universe_level_subst + val subtyping_susbst : t -> universe_instance end @@ -238,8 +238,6 @@ val is_empty_level_subst : universe_level_subst -> bool (** Substitution of universes. *) val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe -val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance -val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints (** Level to universe substitutions. *) |