diff options
| author | Pierre-Marie Pédrot | 2021-01-06 16:29:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-18 13:36:46 +0100 |
| commit | a47e7822338bf0d2ab21c1f9a3b8bfef7a9b50b4 (patch) | |
| tree | 9d9e2b4625dccf3bc424b0e7de594c47c668cdbc /pretyping/reductionops.ml | |
| parent | 875e410294503b03f0954c94164bd611a5682850 (diff) | |
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.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 6 |
1 files 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] |