From a5529d6bdf015aef6b67aab8dd392075e721290b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 4 Oct 2000 15:56:30 +0000
Subject: Utilisation de local_strong plutôt que strong buggé avec défs locales

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

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index f54a8abb0f..1f2a412a2e 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" >];
-  strong whd_betaiotaevar pts.tpf.goal.evar_env (ts_it pts.tpfsigma) pfterm
+  local_strong (whd_betaiotaevar (ts_it pts.tpfsigma)) pfterm
 
 
 (* Focus on the first leaf proof in a proof-tree state *)
-- 
cgit v1.2.3