From 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 29 Oct 2020 13:59:45 +0100
Subject: Move evaluable_global_reference from Names to Tacred.

It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.

In any case this type does not belong to the kernel.
---
 printing/printer.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 732af5570d..524c715455 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -154,7 +154,7 @@ val pr_existential_key     : evar_map -> Evar.t -> Pp.t
 val pr_existential         : env -> evar_map -> existential -> Pp.t
 val pr_constructor         : env -> constructor -> Pp.t
 val pr_inductive           : env -> inductive -> Pp.t
-val pr_evaluable_reference : evaluable_global_reference -> Pp.t
+val pr_evaluable_reference : Tacred.evaluable_global_reference -> Pp.t
 
 val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
 val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
-- 
cgit v1.2.3