diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.mli | 6 |
2 files changed, 0 insertions, 14 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 6614d60276..02b02db893 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1292,14 +1292,6 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) -let instantiate_cumulativity_info (univcst, subtpcst) = - (instantiate_univ_context univcst, instantiate_univ_context subtpcst) - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> diff --git a/kernel/univ.mli b/kernel/univ.mli index 53297ac462..99092a543e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -461,12 +461,6 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs val make_abstract_instance : abstract_universe_context -> universe_instance -(** Don't use. *) -val instantiate_univ_context : abstract_universe_context -> universe_context - -(** Don't use. *) -val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info - (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds |