From 404291584e861cc0f41a5585280143d2df78bd26 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:33:44 +0200
Subject: Remove [constr_of_global_in_context] in funind

---
 plugins/funind/recdef.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'plugins/funind/recdef.ml')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa333c629..ca3160f4c4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -24,6 +24,7 @@ open Globnames
 open Nameops
 open CErrors
 open Util
+open UnivGen
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,7 +51,7 @@ open Context.Rel.Declaration
 (* Ugly things which should not be here *)
 
 [@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
   Coqlib.find_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -62,7 +63,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    UnivGen.constr_of_global @@
+    constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 [@@@ocaml.warning "+3"]
 
@@ -96,9 +97,6 @@ let type_of_const sigma t =
       Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
-let constr_of_global x = 
-  fst (Global.constr_of_global_in_context (Global.env ()) x)
-
 let constant sl s = constr_of_global (find_reference sl s)
 
 let const_of_ref = function
-- 
cgit v1.2.3