From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 21:51:23 +0200
Subject: Safer API for Global.body_of_constant and variants.

We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
---
 printing/prettyp.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ff12737f66..d1e51c9f3c 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -557,9 +557,10 @@ let print_constant with_values sep sp =
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
 	Printer.pr_universe_ctx sigma univs
-    | _ ->
+    | Some (c, ctx) ->
+        let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
-	(if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
         Printer.pr_universe_ctx sigma univs)
 
 let gallina_print_constant_with_infos sp =
-- 
cgit v1.2.3