From c13a9b5eb6479cbd35b90516e623b0a41ad22667 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 12 Jul 2012 15:44:01 +0000
Subject: evar reduction is already made by whd_*

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a011407959..871e676a23 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -57,14 +57,7 @@ let eval_flexible_term ts env c =
   | _ -> assert false
 
 let evar_apprec ts env evd stack c =
-  let sigma =  evd in
-  let rec aux s =
-    let (t,stack) = whd_betaiota_deltazeta_for_iota_state ts env sigma s in
-    match kind_of_term t with
-      | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
-	  aux (Evd.existential_value sigma ev, stack)
-      | _ -> decompose_app (zip (t, stack))
-  in aux (c, append_stack_app_list stack empty_stack)
+  decompose_app (zip (whd_betaiota_deltazeta_for_iota_state ts env evd (c,append_stack_app_list stack empty_stack)))
 
 let apprec_nohdbeta ts env evd c =
   match kind_of_term (fst (Reductionops.whd_stack evd c)) with
-- 
cgit v1.2.3