From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 May 2018 17:44:34 +0200 Subject: Remove some occurrences of Evd.empty We address the easy ones, but they should probably be all removed. --- plugins/omega/coq_omega.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index e455ebb28..3594c8765 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -369,8 +369,11 @@ let coq_True = lazy (init_constant "True") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with - | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> +let evaluable_ref_of_constr s c = + let env = Global.env () in + let evd = Evd.from_env env in + match EConstr.kind evd (Lazy.force c) with + | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) -- cgit v1.2.3