From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 proofs/evar_refiner.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'proofs/evar_refiner.ml')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d19d81e0..f4613f8d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
 
 open Util
 open Names
@@ -15,6 +15,7 @@ open Evd
 open Sign
 open Proof_trees
 open Refiner
+open Pretyping
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -22,21 +23,21 @@ open Refiner
 
 (* w_tactic pour instantiate *) 
 
-let w_refine evk rawc evd =
+let w_refine evk (ltac_vars,rawc) evd =
   if Evd.is_defined (evars_of evd) evk then 
     error "Instantiate called on already-defined evar";
   let e_info = Evd.find (evars_of evd) evk in
   let env = Evd.evar_env e_info in
-  let sigma,typed_c =
-    try Pretyping.Default.understand_tcc ~resolve_classes:false
-      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
+  let evd',typed_c =
+    try Pretyping.Default.understand_ltac 
+      (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
       user_err_loc 
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    evar_define evk typed_c (evars_reset_evd sigma evd)
+    evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
 
 (* vernac command Existential *)
 
@@ -55,5 +56,5 @@ let instantiate_pf_com n com pfts =
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_goal_evar_defs sigma in
-  let evd' = w_refine evk rawc evd in
+  let evd' = w_refine evk (([],[]),rawc) evd in
     change_constraints_pftreestate (evars_of evd') pfts
-- 
cgit v1.2.3