Fix type class discharge again.

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

1 files changed, 2 insertions, 1 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1b8c5a2331..96e36b70ba 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -139,12 +139,13 @@ let discharge_class (_,cl) =
 	(decl :: ctx', n :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
+    let rel = map_rel_context (Cooking.expmod_constr repl) rel in
     let ctx, _ =
       List.fold_right
 	(fun (id, b, t) (ctx, k) ->
 	   (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
 	rel ([], n)
-    in map_rel_context (Cooking.expmod_constr repl) ctx
+    in ctx
   in
   let abs_context cl =
     match cl.cl_impl with