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 ---
 tactics/cbn.ml             | 12 ++++++++++++
 tactics/cbn.mli            |  7 +++++++
 tactics/redexpr.ml         |  7 ++-----
 5 files changed, 21 insertions(+), 20 deletions(-)

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 } *)
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 39959d6fb8..6fb6cff04f 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -820,3 +820,15 @@ let whd_cbn flags env sigma t =
     (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty))
   in
   Stack.zip ~refold:true sigma state
+
+let norm_cbn 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 (whd_cbn flags env sigma t) in
+  strongrec env t
diff --git a/tactics/cbn.mli b/tactics/cbn.mli
index af54771382..a02a74f9e4 100644
--- a/tactics/cbn.mli
+++ b/tactics/cbn.mli
@@ -8,6 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(** Weak-head cbn reduction. Despite the name, the cbn reduction is a complex
+    reduction distinct from call-by-name or call-by-need. *)
 val whd_cbn :
   CClosure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
+
+(** Strong variant of cbn reduction. *)
+val norm_cbn :
+  CClosure.RedFlags.reds ->
+  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index b415b30de8..87cae3abe5 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -46,9 +46,6 @@ let cbv_native env sigma c =
 
 let whd_cbn = Cbn.whd_cbn
 
-let strong_cbn flags =
-  strong_with_flags whd_cbn flags
-
 let simplIsCbn =
   Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false
 
@@ -248,11 +245,11 @@ let reduction_of_red_expr_val = function
   | Hnf -> (e_red hnf_constr,DEFAULTcast)
   | Simpl (f,o) ->
      let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
-     let am = if simplIsCbn () then strong_cbn f else simpl in
+     let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
   | Cbn f ->
-     (e_red (strong_cbn f), DEFAULTcast)
+     (e_red (Cbn.norm_cbn f), DEFAULTcast)
   | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
   | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
   | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
-- 
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 ++++-
 tactics/tactics.ml         | 4 ----
 4 files changed, 7 insertions(+), 15 deletions(-)

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 *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40bdbc25e..aef6596e8f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1244,8 +1244,6 @@ let force_destruction_arg with_evars env sigma c =
 (* tactic "cut" (actually modus ponens) *)
 (****************************************)
 
-let normalize_cut = false
-
 let cut c =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1260,8 +1258,6 @@ let cut c =
     | sigma, s ->
       let r = Sorts.relevance_of_sort s in
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
-      (* Backward compat: normalize [c]. *)
-      let c = if normalize_cut then strong whd_betaiota env sigma c else c in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
         (Refine.refine ~typecheck:false begin fun h ->
             let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
-- 
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(-)

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