diff options
| author | herbelin | 2009-12-14 19:05:05 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-14 19:05:05 +0000 |
| commit | cc5c3eb26f817a0a1cd479c0f7f3083e648b9a9b (patch) | |
| tree | d5de785d0560bb7c867560e8b09408b7f24a117e /pretyping | |
| parent | f698148f6aee01a207ce5ddd4bebf19da2108bff (diff) | |
Improved strategy for rewriting lemma possibly depending because of evars.
Explained in CHANGES how to cope with the change of semantics of
abbreviations wrt implicit arguments positions propagation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12586 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |