From 34bcd562cc9c8e5e6b0f3b79a15b9c55dd98813e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 15:29:10 +0200
Subject: The only abstraction-breaking function in Univ is now
 AUContext.instance.

---
 kernel/univ.ml  | 8 --------
 kernel/univ.mli | 6 ------
 2 files changed, 14 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3