From 8f72678f7a1fc1d0e2c9ac7a5f682ce100bfa403 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Jun 2009 18:59:06 +0000
Subject: Use a lazy value for the message in FailError, so that it won't be
 unnecessarily computed when the user won't see it (avoids the costly
 nf_evar_defs in typeclass errors). Add hook support for mutual definitions in
 Program. Try to solve only the argument typeclasses when calling [refine].

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

(limited to 'pretyping/typeclasses_errors.ml')

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index f1a57ffc16..c7e3895e06 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
     | None ->
 	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
     | Some ev ->
-	let evi = Evd.find ( evd) ev in
+	let evi = Evd.find evd ev in
 	let loc, kind = Evd.evar_source ev evd in
 	  raise (Stdpp.Exc_located (loc, TypeClassError
 	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
-- 
cgit v1.2.3