diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-30 15:18:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-01 17:26:02 +0200 |
| commit | 3e1e8e5792b43be83da2cca8102418aa9b73b9b3 (patch) | |
| tree | f46ebf80ac216adddf32bff2386114e0bf4d5ef0 /pretyping | |
| parent | e57aab0559297cff3875931258674cfe2cfbbba3 (diff) | |
Make semantics of whd_zeta consistent with other whd_* functions.
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3f89acf33..29b448caa 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 e7a6b3d64..fdfa77412 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 *) |