diff options
| author | msozeau | 2009-04-27 16:50:42 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-27 16:50:42 +0000 |
| commit | e9667ab2ee2b05e54030345668c13fa363a399d9 (patch) | |
| tree | d157af03964c8eff15b28fb7a587fc9c8d420d4b /pretyping/typeclasses.ml | |
| parent | 94affd965c1554d2ad10654e9832fcdb2a024daf (diff) | |
- 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
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |