From 5dcf8f4d0fb7419c07b9287db22f6ed6cbf000a4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Jan 2021 16:08:16 +0100
Subject: Move the only use of strong_with_flags to its single calling module.

This also allows to move the strong variant of cbn to the Cbn module.
---
 pretyping/reductionops.ml  | 12 ------------
 pretyping/reductionops.mli |  3 ---
 2 files changed, 15 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3da75f67b9..d52be18faa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -468,18 +468,6 @@ let safe_meta_value sigma ev =
   try Some (Evd.meta_value sigma ev)
   with Not_found -> None
 
-let strong_with_flags whdfun flags env sigma t =
-  let push_rel_check_zeta d env =
-    let open CClosure.RedFlags in
-    let d = match d with
-      | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
-      | d -> d in
-    push_rel d env in
-  let rec strongrec env t =
-    map_constr_with_full_binders env sigma
-      push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
-  strongrec env t
-
 let strong whdfun env sigma t =
   let rec strongrec env t =
     map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 59bc4a8b72..93cb4c190c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -145,9 +145,6 @@ type stack_reduction_function =
 
 (** {6 Reduction Function Operators } *)
 
-val strong_with_flags :
-  (CClosure.RedFlags.reds -> reduction_function) ->
-  (CClosure.RedFlags.reds -> reduction_function)
 val strong : reduction_function -> reduction_function
 
 (** {6 Generic Optimized Reduction Function using Closures } *)
-- 
cgit v1.2.3


From 875e410294503b03f0954c94164bd611a5682850 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Jan 2021 16:20:04 +0100
Subject: Move the two only calls to the strong combinator to their calling
 site.

---
 pretyping/reductionops.ml  | 9 +++------
 pretyping/reductionops.mli | 4 ----
 pretyping/tacred.ml        | 5 ++++-
 3 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d52be18faa..6185cd3280 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -468,11 +468,6 @@ let safe_meta_value sigma ev =
   try Some (Evd.meta_value sigma ev)
   with Not_found -> None
 
-let strong whdfun env sigma t =
-  let rec strongrec env t =
-    map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in
-  strongrec env t
-
 (*************************************)
 (*** Reduction using bindingss ***)
 (*************************************)
@@ -1269,7 +1264,9 @@ let plain_instance sigma s c = match s with
 
 let instance env sigma s c =
   (* if s = [] then c else *)
-  strong whd_betaiota env sigma (plain_instance sigma s c)
+  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)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 93cb4c190c..140ebdc87d 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -143,10 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 type stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
 
-(** {6 Reduction Function Operators } *)
-
-val strong : reduction_function -> reduction_function
-
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 01819a650b..bd21ecef93 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1040,7 +1040,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
 let whd_simpl env sigma c =
   applist (whd_simpl_stack env sigma (c, []))
 
-let simpl env sigma c = strong whd_simpl env sigma c
+let simpl env sigma c =
+  let rec strongrec env t =
+    map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in
+  strongrec env c
 
 (* Reduction at specific subterms *)
 
-- 
cgit v1.2.3


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(-)

(limited to 'pretyping')

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