From bc6a92bbcf13044719e3dfd0f2575d07a0cc9036 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Oct 2000 16:10:07 +0000
Subject: Utilisation de local_strong plutôt que strong buggé avec défs locales
 (2ème)

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

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1f2a412a2e..af3f15ef48 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -681,7 +681,7 @@ let extract_pftreestate pts =
   if subgoals <> [] then
    errorlabstrm "extract_proof"
    [< 'sTR "Attempt to save an incomplete proof" >];
-  local_strong (whd_betaiotaevar (ts_it pts.tpfsigma)) pfterm
+  local_strong (whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma)) pfterm
 
 
 (* Focus on the first leaf proof in a proof-tree state *)
-- 
cgit v1.2.3