diff options
Diffstat (limited to 'checker/univ.ml')
| -rw-r--r-- | checker/univ.ml | 19 |
1 files changed, 1 insertions, 18 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index fa884d9d06..525f535e92 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 = |