From 9a5c74b8229f90b2ac1df5c41f7857cc1b0bf067 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 15 Nov 2009 20:24:19 +0000
Subject: Fix type class discharge again.

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

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
-- 
cgit v1.2.3