From 317af3e75771d5fdcb5fb8d35d2aa5bd196c432f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 Oct 2000 13:18:23 +0000
Subject: Essai de remplacement du whd_betaiotaevar de Qed par un whd_ise

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

(limited to 'proofs')

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