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.

---
 printing/prettyp.ml  |  7 +++++--
 printing/printmod.ml | 15 +++++++++++++--
 2 files changed, 18 insertions(+), 4 deletions(-)

(limited to 'printing')

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