From 6b2d99445d35ea71cd24becb7f936e0cc9779d46 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 8 Feb 2001 08:29:12 +0000
Subject: simplification du make depend; fonctions de stat. util. memoire dans
 certains modules

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

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fca4d85fe5..37a41cd257 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -664,10 +664,11 @@ 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))*)
-  local_strong (whd_ise (ts_it pts.tpfsigma))
-    pfterm
-
+  (***  
+  let env = Global.env_of_context pts.tpf.goal.evar_hyps in
+  strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm
+  ***)
+  local_strong (whd_ise (ts_it pts.tpfsigma)) pfterm
 
 (* Focus on the first leaf proof in a proof-tree state *)
 
-- 
cgit v1.2.3