diff options
| -rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 35 |
2 files changed, 10 insertions, 33 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3352bfce38..7a5d0897b5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -930,14 +930,6 @@ let stack_red_of_state_red f = let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f -(* Drops the Cst_stack *) -let iterate_whd_gen flags env sigma s = - let rec aux t = - let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in - let whd_sk = Stack.map aux sk in - Stack.zip sigma (hd,whd_sk) - in aux s - let red_of_state_red f env sigma x = Stack.zip sigma (f env sigma (x,Stack.empty)) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..04dfc5ffe6 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -106,8 +106,6 @@ end (************************************************************************) -type state = constr * constr Stack.t - type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type state_reduction_function = - env -> evar_map -> state -> state - -val pr_state : env -> evar_map -> state -> Pp.t - (** {6 Reduction Function Operators } *) val strong_with_flags : @@ -127,12 +120,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val whd_state_gen : - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state - -val iterate_whd_gen : CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> constr -> constr - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function val whd_allnolet_stack : stack_reduction_function val whd_betalet_stack : stack_reduction_function -val whd_nored_state : state_reduction_function -val whd_beta_state : state_reduction_function -val whd_betaiota_state : state_reduction_function -val whd_betaiotazeta_state : state_reduction_function -val whd_all_state : state_reduction_function -val whd_allnolet_state : state_reduction_function -val whd_betalet_state : state_reduction_function - (** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function -val whd_delta_state : state_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function -val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function val whd_zeta_stack : stack_reduction_function -val whd_zeta_state : state_reduction_function val whd_zeta : reduction_function val shrink_eta : Environ.env -> constr -> constr @@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (** {6 Heuristic for Conversion with Evar } *) +type state = constr * constr Stack.t + +type state_reduction_function = + env -> evar_map -> state -> state + +val pr_state : env -> evar_map -> state -> Pp.t + +val whd_nored_state : state_reduction_function + val whd_betaiota_deltazeta_for_iota_state : - TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state + TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr |