2 files changed, 8 insertions, 4 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index febfb04947..f9ab283ada 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,6 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types =
 	let evm' = Evd.evars_of evd' in
 	  match Evd.evar_body (Evd.find evm' ev) with
 	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
+	    | Evar_defined c -> Evarutil.nf_evar evm' c
       else raise Not_found
   with Exit -> raise Not_found
 
@@ -278,6 +279,8 @@ let destClassApp c =
     | _ -> None
 
 let resolve_typeclasses ?(check=true) env sigma evd =
+(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
+(*   with _ -> *)
   let evm = Evd.evars_of evd in
   let tc_evars = 
     let f ev evi acc =
@@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
 	(fun ev evi acc -> 
 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
 	    resolve_typeclass env ev evi acc 
-	  else acc) 
+	  else acc)
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
       else
 	sat (Evarutil.nf_evar_defs evars')
-  in sat evd
-
+  in sat (Evarutil.nf_evar_defs evd)
+  
 let class_of_constr c = 
   let extract_ind c =
     match kind_of_term c with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ec3350a586..db408c8898 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -64,6 +64,7 @@ val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_def
 val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
+val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref
 
 type substitution = (identifier * constr) list