From cc099cc1b2f1370ec1d8f57c54c29045513b583b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 29 Jun 2010 22:21:33 +0000
Subject: Correct wrong handling of evars in instance definitions that
 prevented information going from the body to the type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13224 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 62a7ebb445..9c21366d28 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -146,7 +146,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
     let (env', ctx), imps = interp_context_evars evars env ctx in
-    let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+    let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
-- 
cgit v1.2.3