From 27a9a28e8628c94910a08efc2f611e91e3e553bb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Jan 2021 12:09:19 +0100
Subject: Respect print_universes in detype_instance

This partially fixes #13732 and matches what we do in detype_sort
---
 pretyping/detyping.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb5125f5ed..666784f368 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -744,9 +744,11 @@ let detype_level sigma l =
   UNamed (detype_level_name sigma l)
 
 let detype_instance sigma l =
-  let l = EInstance.kind sigma l in
-  if Univ.Instance.is_empty l then None
-  else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
+  if not !print_universes then None
+  else
+    let l = EInstance.kind sigma l in
+    if Univ.Instance.is_empty l then None
+    else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g =
   match d with
-- 
cgit v1.2.3