From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 19 Feb 2009 13:13:14 +0100
Subject: Imported Upstream version 8.2-1+dfsg

---
 proofs/logic.ml   | 8 ++++----
 proofs/refiner.ml | 4 ++--
 proofs/tacmach.ml | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index a04216cb..3e758eb6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	let conclty = nf_betaiota conclty in
+	let conclty = nf_betaiota sigma conclty in
 	  if !check && occur_meta conclty then
 	    raise (RefinerError (MetaInType conclty));
 	  (mk_goal hyps conclty)::goalacc, conclty
@@ -390,7 +390,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
+	(mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
@@ -502,7 +502,7 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 	
     | Cut (b,replace,id,t) ->
-        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg1 = mk_goal sign (nf_betaiota sigma t) in
 	let sign,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a9a1f51d..7ce256bf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
+(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -763,7 +763,7 @@ let extract_pftreestate pts =
       else
         str "Attempt to save a proof with existential variables still non-instantiated");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
-  nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+  nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
   (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
   (***
   local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index bf194d47..6c4f7b5e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -99,7 +99,7 @@ let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce nf
-let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of
-- 
cgit v1.2.3