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