From cc5c3eb26f817a0a1cd479c0f7f3083e648b9a9b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Dec 2009 19:05:05 +0000
Subject: 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
---
 pretyping/reductionops.ml  | 7 ++++++-
 pretyping/reductionops.mli | 1 +
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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 *)
 
-- 
cgit v1.2.3