From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/omega/coq_omega.ml | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

(limited to 'plugins/omega/coq_omega.ml')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 51cd665f..e14c4e2e 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -18,8 +18,8 @@
 open CErrors
 open Util
 open Names
+open Constr
 open Nameops
-open Term
 open EConstr
 open Tacticals.New
 open Tacmach.New
@@ -29,7 +29,7 @@ open Libnames
 open Globnames
 open Nametab
 open Contradiction
-open Misctypes
+open Tactypes
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -38,15 +38,9 @@ open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
 
-let elim_id id =
-  Proofview.Goal.enter begin fun gl ->
-    simplest_elim (mkVar id)
-  end
-let resolve_id id = Proofview.Goal.enter begin fun gl ->
-  apply (mkVar id)
-end
+let elim_id id = simplest_elim (mkVar id)
 
-let timing timer_name f arg = f arg
+let resolve_id id = apply (mkVar id)
 
 let display_time_flag = ref false
 let display_system_flag = ref false
@@ -206,7 +200,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
+let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
@@ -369,8 +363,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