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/hints.ml   | 2 +-
 tactics/redexpr.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index f49b1660b8..7eeee7ee07 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1064,7 +1064,7 @@ let subst_autohint (subst, obj) =
   in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
-    let pat' = Option.Smart.map (subst_pattern subst) data.pat in
+    let pat' = Option.Smart.map (subst_pattern (Global.env()) subst) data.pat in
     let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
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