From a47e7822338bf0d2ab21c1f9a3b8bfef7a9b50b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Jan 2021 16:29:50 +0100
Subject: Do not call the with_full_binder map variant for Reduction.instance.

We know statically that whd_betaiota is a local reduction function, so it
does not need to access the rel_context of its environment argument.
---
 pretyping/reductionops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6185cd3280..d4866541b0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1264,9 +1264,9 @@ let plain_instance sigma s c = match s with
 
 let instance env sigma s c =
   (* if s = [] then c else *)
-  let rec strongrec env t =
-    map_constr_with_full_binders env sigma push_rel strongrec env (whd_betaiota env sigma t) in
-  strongrec env (plain_instance sigma s c)
+  (* No need to compute contexts under binders as whd_betaiota is local *)
+  let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in
+  strongrec (plain_instance sigma s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
-- 
cgit v1.2.3