diff options
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 |
3 files changed, 8 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3f89acf332..29b448caa3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1148,7 +1148,9 @@ let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) -let whd_zeta c = Stack.zip (local_whd_state_gen Closure.zeta Evd.empty (c,Stack.empty)) +let whd_zeta_state = local_whd_state_gen Closure.zeta +let whd_zeta_stack = stack_red_of_state_red whd_zeta_state +let whd_zeta = red_of_state_red whd_zeta_state (****************************************************************************) (* Reduction Functions *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e7a6b3d648..fdfa77412e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -187,9 +187,11 @@ 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 : local_stack_reduction_function +val whd_zeta_state : local_state_reduction_function +val whd_zeta : local_reduction_function val shrink_eta : constr -> constr -val whd_zeta : constr -> constr (** Various reduction functions *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 1950356b38..24028b09df 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -400,7 +400,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let isatomic = isProd (whd_zeta hdcncl) in + let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let isatomic = isProd (whd_zeta evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in |