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

---
 tactics/tactics.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5af5c0d5..2c567034 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -759,7 +759,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let concl_nprod = nb_prod (pf_concl gl0) in
   let evm, c = c in
   let rec try_main_apply c gl =
-    let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+    let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
     let try_apply thm_ty nprod =
       let n = nb_prod thm_ty - nprod in
 	if n<0 then error "Applied theorem has not enough premisses.";
@@ -850,7 +850,7 @@ let progress_with_clause flags innerclause clause =
   with Failure _ -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause (d,lbind) gl =
-  let thm = nf_betaiota (pf_type_of gl d) in
+  let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with err ->
@@ -985,7 +985,8 @@ let specialize mopt (c,lbind) g =
     else 
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
-      let (thd,tstack) = whd_stack (clenv_value clause) in
+      let (thd,tstack) =
+        whd_stack (evars_of clause.evd) (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m -> 
-- 
cgit v1.2.3