From bf5f0520cf105afb048c6eac5d6de1d3e1a719df Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 21:06:34 +0200
Subject: Remove one call to Global.env in Detyping

One other call still remains, but will require to refactor some
section-handling code.
---
 tactics/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/redexpr.ml')

diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index aabfae444e..7ff88bb4b7 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -262,7 +262,7 @@ let subst_red_expr subs =
   Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Patternops.subst_pattern subs)
+    (Patternops.subst_pattern (Global.env()) subs)
 
 let inReduction : bool * string * red_expr -> obj =
   declare_object
-- 
cgit v1.2.3


From 61d53a17c594de1ea37b37f6215319d996ec31ea Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 10:02:18 +0200
Subject: Remove calls to Global.env in Patternops

---
 tactics/redexpr.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics/redexpr.ml')

diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 7ff88bb4b7..447b908a1d 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -259,10 +259,12 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Patternops.subst_pattern (Global.env()) subs)
+    (Patternops.subst_pattern env sigma subs)
 
 let inReduction : bool * string * red_expr -> obj =
   declare_object
-- 
cgit v1.2.3