diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 7 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
2 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bbc0ceae7d..d5bc868894 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -219,6 +219,7 @@ open RedFlags (* Local *) let beta = mkflags [fbeta] let eta = mkflags [feta] +let zeta = mkflags [fzeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] @@ -495,10 +496,14 @@ let whd_betadeltaiota_nolet_stack env = let whd_betadeltaiota_nolet env = red_of_state_red (whd_betadeltaiota_nolet_state env) -(* 3. Eta reduction Functions *) +(* 4. Eta reduction Functions *) let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack)) +(* 5. Zeta Reduction Functions *) + +let whd_zeta c = app_stack (local_whd_state_gen zeta Evd.empty (c,empty_stack)) + (****************************************************************************) (* Reduction Functions *) (****************************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1268a3f3b5..9e5ced8a28 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -136,6 +136,7 @@ val whd_betadeltaiotaeta_state : state_reduction_function val whd_betadeltaiotaeta : reduction_function val whd_eta : constr -> constr +val whd_zeta : constr -> constr (* Various reduction functions *) |