From 6160f53e89800a785d773c4130b08fbe7c345651 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 6 Feb 2009 21:25:52 +0000
Subject: pushed evar reduction in kernel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/showproof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index cf861642db..2ab62763d4 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree =
                        {ihsg=No_subgoals_hyp;isgintro=""}
                        (List.nth ltree 0))]
         ]
-and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and whd_betadeltaiota x = whd_betaiota Evd.empty x
 and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
 and prod_head t =
   match (kind_of_term (strip_outer_cast t)) with 
-- 
cgit v1.2.3