From e9667ab2ee2b05e54030345668c13fa363a399d9 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 27 Apr 2009 16:50:42 +0000
Subject: - Implementation of a new typeclasses eauto procedure based on
 success   and failure continuations, allowing to do safe cuts correctly. -
 Fix bug #2097 by suppressing useless nf_evars calls. - Improve the proof
 search strategy used by rewrite for subrelations and   fix some hints. Up to
 20% speed improvement in setoid-intensive files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 56b78715ad..219f9d1277 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -332,9 +332,8 @@ let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
-  if not (has_typeclasses ( evd)) then evd
-  else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+  if not (has_typeclasses evd) then evd
+  else !solve_instanciations_problem env evd onlyargs split fail
 
 let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
-- 
cgit v1.2.3