Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.

2 files changed, 15 insertions, 7 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 15c0f80b9..d9bb97be1 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,8 @@ let print_ref reduce ref =
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
+  let inst = Univ.AUContext.instance univs in
+  let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
   let bl = Universes.universe_binders_of_global ref in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
@@ -503,7 +505,10 @@ let ungeneralized_type_of_constant_type t =
 
 let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
-    pr_universe_instance sigma (Declareops.constant_polymorphic_context cb)
+    let univs = Declareops.constant_polymorphic_context cb in
+    let inst = Univ.AUContext.instance univs in
+    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    pr_universe_instance sigma univs
   else mt()
 				
 let print_constant with_values sep sp =
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 10b791e37..2e0e6d284 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -89,7 +89,7 @@ let build_ind_type env mip =
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
@@ -100,7 +100,9 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
-      Printer.pr_universe_instance sigma (Declareops.inductive_polymorphic_context mib)
+      let ctx = Declareops.inductive_polymorphic_context mib in
+      let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+      Printer.pr_universe_instance sigma ctx
     else mt ()
   in
   hov 0 (
@@ -149,7 +151,7 @@ let get_fields =
 let print_record env mind mib =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
-      Declareops.inductive_polymorphic_instance mib
+      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
     else Univ.Instance.empty 
   in
   let mip = mib.mind_packets.(0) in
@@ -292,11 +294,13 @@ let print_body is_impl env mp (l,body) =
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
+       let ctx = Declareops.constant_polymorphic_context cb in
        let u =
 	 if Declareops.constant_is_polymorphic cb then
-            Declareops.constant_polymorphic_instance cb
+            Univ.AUContext.instance ctx
 	 else Univ.Instance.empty
        in
+       let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
        let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
@@ -316,8 +320,7 @@ let print_body is_impl env mp (l,body) =
 		       Printer.pr_lconstr_env env sigma
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx sigma 
-              (Declareops.constant_polymorphic_context cb))
+	    Printer.pr_universe_ctx sigma ctx)
     | SFBmind mib ->
       try
 	let env = Option.get env in