From 908900165bc6a5b2eb9bc4f177311ee2409dbd6a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 3 Jun 2008 23:08:00 +0000
Subject: Fixes incorrect handling of existing existentials variables in 
 typeclass code.

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

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 226cb3f012..855d388c43 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -28,8 +28,8 @@ let w_refine ev rawc evd =
   let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    try Pretyping.Default.understand_tcc (evars_of evd) env 
-      ~expected_type:e_info.evar_concl rawc 
+    try Pretyping.Default.understand_tcc ~resolve_classes:false
+      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
     with _ -> error ("The term is not well-typed in the environment of " ^
 			string_of_existential ev)
   in
-- 
cgit v1.2.3