Minor fixes in typeclasses:

- Set implicit args on for Context decls
- Move class_apply tactic to Init
- Normalize evars before raising an error.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 0 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2d5cd659f..10283e529 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -258,6 +258,7 @@ let named_of_rel_context l =
   in ctx
 
 let context ?(hook=fun _ -> ()) l =
+  Impargs.make_manual_implicit_args true;
   let env = Global.env() in
   let evars = ref Evd.empty in
   let (env', fullctx), impls = interp_context_evars evars env l in