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.
---
 plugins/omega/coq_omega.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4f7b3fbe74..9d92ffde74 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -354,8 +354,9 @@ let coq_True = gen_constant "core.True.type"
 let evaluable_ref_of_constr s c =
   let env = Global.env () in
   let evd = Evd.from_env env in
+  let open Tacred in
   match EConstr.kind evd (Lazy.force c) with
-  | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
+  | Const (kn,u) when is_evaluable env (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
 
-- 
cgit v1.2.3