From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 proofs/evar_refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/evar_refiner.ml')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36268de1..6fa95dc8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -40,7 +40,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     error "Instantiate called on already-defined evar";
   let env = Evd.evar_env evi in
   let sigma',typed_c =
-    try Pretyping.Default.understand_ltac true sigma env ltac_var
+    try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Glob_term.loc_of_glob_constr rawc in
-- 
cgit v1.2.3