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.

3 files changed, 21 insertions, 5 deletions

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)