From 459fe01a4163a7b7a73d0774270a1331a7721736 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Mar 2014 21:39:05 +0100
Subject: Potentially unused computation in Goal.

---
 proofs/goal.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 07bdbda00b..b0fded2890 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -374,8 +374,11 @@ let defs _ rdefs _ _ =
   !rdefs
 
 let enter f = (); fun env rdefs gl info ->
-  let info = Evarutil.nf_evar_info !rdefs info in
-  f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info) gl
+  let sigma = !rdefs in
+  let concl = Reductionops.nf_evar sigma (Evd.evar_concl info) in
+  let map_nf c = Reductionops.nf_evar sigma c in
+  let hyps = Environ.map_named_val map_nf (Evd.evar_hyps info) in
+  f env sigma hyps concl gl
 
 (*** Conversion in goals ***)
 
-- 
cgit v1.2.3