From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 19:11:20 +0200
Subject: 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.
---
 printing/prettyp.ml  |  7 ++++++-
 printing/printmod.ml | 15 +++++++++------
 2 files changed, 15 insertions(+), 7 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 15c0f80b93..d9bb97be10 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 10b791e37f..2e0e6d2845 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
-- 
cgit v1.2.3


From 91df402729f70144a4e4d198c4384dc515920e59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 15:42:43 +0200
Subject: Moving the last bits of abtraction-breaking code out of the kernel.

---
 printing/prettyp.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d9bb97be10..ff12737f66 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -514,7 +514,16 @@ let print_instance sigma cb =
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
-  let typ = Declareops.type_of_constant cb in
+  let typ = match cb.const_type with
+  | RegularArity t as x ->
+    begin match cb.const_universes with
+    | Monomorphic_const _ -> x
+    | Polymorphic_const univs ->
+      let inst = Univ.AUContext.instance univs in
+      RegularArity (Vars.subst_instance_constr inst t)
+    end
+  | TemplateArity _ as x -> x
+  in
   let typ = ungeneralized_type_of_constant_type typ in
   let univs =
     let otab = Global.opaque_tables () in
-- 
cgit v1.2.3