From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 23:48:28 +0100
Subject: Moving printing code from Evd to Termops.

---
 pretyping/detyping.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d4e156fa4b..c8d945c0b5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -422,7 +422,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,7 +434,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+  GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
@@ -533,7 +533,7 @@ let rec detype flags avoid env sigma t =
       let id,l =
         try
           let id = match Evd.evar_ident evk sigma with
-          | None -> Evd.pr_evar_suggested_name evk sigma
+          | None -> Termops.pr_evar_suggested_name evk sigma
           | Some id -> id
           in
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
-- 
cgit v1.2.3