The only abstraction-breaking function in Univ is now AUContext.instance.

5 files changed, 19 insertions, 19 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
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index a0c88a7af1..5cd79ed6df 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -532,7 +532,9 @@ let print_constant with_values sep sp =
       begin
         match cb.const_universes with
         | Monomorphic_const ctx -> ctx
-        | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+        | Polymorphic_const ctx ->
+          let inst = Univ.AUContext.instance ctx in
+          Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
@@ -542,7 +544,8 @@ let print_constant with_values sep sp =
         Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
       | Polymorphic_const ctx ->
         assert(Univ.ContextSet.is_empty body_uctxs);
-        Univ.instantiate_univ_context ctx
+        let inst = Univ.AUContext.instance ctx in
+        Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
   in
   let ctx =
     Evd.evar_universe_context_of_binders
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2e0e6d2845..5c7dcdc10f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -110,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
+let instantiate_cumulativity_info cumi =
+  let open Univ in
+  let univs = ACumulativityInfo.univ_context cumi in
+  let subtyp = ACumulativityInfo.subtyp_context cumi in
+  let expose ctx =
+    let inst = AUContext.instance ctx in
+    let cst = AUContext.instantiate inst ctx in
+    UContext.make (inst, cst)
+  in
+  CumulativityInfo.make (expose univs, expose subtyp)
+
 let print_mutual_inductive env mind mib =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
@@ -133,7 +144,7 @@ let print_mutual_inductive env mind mib =
          | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
          | Cumulative_ind cumi ->
            Printer.pr_cumulativity_info
-             sigma (Univ.instantiate_cumulativity_info cumi))
+             sigma (instantiate_cumulativity_info cumi))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -191,7 +202,7 @@ let print_record env mind mib =
     | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
     | Cumulative_ind cumi ->
       Printer.pr_cumulativity_info
-        sigma (Univ.instantiate_cumulativity_info cumi)
+        sigma (instantiate_cumulativity_info cumi)
   )
 
 let pr_mutual_inductive_body env mind mib =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 86dcb6d4dc..784c6d3387 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,7 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
+      let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =