From 2c2a1b91e994a4256d1bbebaa405ad114d834206 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 15 Dec 2010 16:43:55 +0000
Subject: Clenv.connect_clenv without its Evd.fold

 Apparently, it seems that clenv.evd is either created
 from dummy_goal (in (e)auto) or from a copy of gls (in
 class_tactics). I've checked experimentally by some assert
 that on the stdlib the defined part of clenv.evd is always
 included in gls. I hence propose to simplify this function
 connect_clenv.

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

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 71d952caf9..4fc6c5b350 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -337,15 +337,7 @@ let evar_clenv_unique_resolver = clenv_unique_resolver
 (******************************************************************)
 
 let connect_clenv gls clenv =
-  let evd = Evd.fold begin fun ev evi acc -> 
-                        if evi.evar_body = Evar_empty then
-			  acc
-			else
-			  Evd.add acc ev evi
-                  end
-                  clenv.evd gls.sigma
-  in
-  let evd = evars_reset_evd evd clenv.evd in
+  let evd = evars_reset_evd gls.sigma clenv.evd in
   { clenv with
     evd = evd ;
     env = Goal.V82.env evd (sig_it gls) }
-- 
cgit v1.2.3