From 3e1e8e5792b43be83da2cca8102418aa9b73b9b3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 30 Jun 2016 15:18:21 +0200
Subject: 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
---
 pretyping/reductionops.ml  | 4 +++-
 pretyping/reductionops.mli | 4 +++-
 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
-- 
cgit v1.2.3