Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.

1 files changed, 5 insertions, 3 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 7795084779..fc398df9aa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -929,9 +929,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
 let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-         DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
+    let ref',t = subst_global subst ref in
+    if ref' == ref then raw else
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
 
   | GSort _
   | GVar _