aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-06-11 18:59:06 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-06-11 18:59:06 +0000
commit8f72678f7a1fc1d0e2c9ac7a5f682ce100bfa403 (patch)
tree4aa74c5721a3b24372cfa0d72784749de204d493 /pretyping
parent80105c8482bd487782dcab8161fa1fc1f3fdf635 (diff)
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
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/typeclasses_errors.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index f1a57ffc1..c7e3895e0 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)))))