From 35521213d7cbd9375e9f7016d57fac9b147e2840 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 18 Apr 2023 15:26:24 +0200 Subject: [PATCH] Remove legacy `let head_style = false` in redexpr --- tactics/redexpr.ml | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 19e08dcd1b2c..2b9f4883a061 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -50,8 +50,6 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) -let whd_cbn = Cbn.whd_cbn - let { Goptions.get = simplIsCbn } = Goptions.declare_bool_option_and_ref ~key:["SimplIsCbn"] @@ -210,18 +208,14 @@ let out_with_occurrences (occs,c) = let e_red f env evm c = evm, f env evm c -let head_style = false (* Turn to true to have a semantics where simpl - only reduce at the head when an evaluable reference is given, e.g. - 2+n would just reduce to S(1+n) instead of S(S(n)) *) - -let contextualize f g = function +let contextuallize f = function | Some (occs,c) -> let l = out_occurrences occs in - let b,c,h = match c with - | Inl r -> true,PRef (global_of_evaluable_reference r),f - | Inr c -> false,c,f in - e_red (contextually b (l,c) (fun _ -> h)) - | None -> e_red g + let b,c = match c with + | Inl r -> true,PRef (global_of_evaluable_reference r) + | Inr c -> false,c in + e_red (contextually b (l,c) (fun _ -> f)) + | None -> e_red f let warn_simpl_unfolding_modifiers = CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:CWarnings.CoreCategories.tactics @@ -251,9 +245,8 @@ let reduction_of_red_expr_val = function else (e_red red_product,DEFAULTcast) | 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 Cbn.norm_cbn f else simpl in - (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) + (contextuallize am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> (e_red (Cbn.norm_cbn f), DEFAULTcast) @@ -266,8 +259,8 @@ let reduction_of_red_expr_val = function with Not_found -> user_err (str "Unknown user-defined reduction \"" ++ str s ++ str "\".")) - | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) - | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) + | CbvVm o -> (contextuallize cbv_vm o, VMcast) + | CbvNative o -> (contextuallize cbv_native o, NATIVEcast) let reduction_of_red_expr env r = reduction_of_red_expr_val (eval_red_expr env r)