From 6aeda23a14a5a5dfca259fe99a19d7bcb42d1052 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Jul 2017 16:47:55 +0200 Subject: Removing a few suspicious functions from the kernel. These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead. --- printing/prettyp.ml | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 6d2bf6b73..51e557f2e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -511,7 +511,25 @@ let print_constant with_values sep sp = let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Global.universes_of_constant_body cb in + let univs = + let otab = Global.opaque_tables () in + match cb.const_body with + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + end + | OpaqueDef o -> + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + 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 + in let ctx = Evd.evar_universe_context_of_binders (Universes.universe_binders_of_global (ConstRef sp)) -- cgit v1.2.3