From 925e99db4166a97056e0ab3c314b452e1f2559cb Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 16 Jan 2009 13:30:37 +0000
Subject: Correct a bug in commit 11659

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

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bf346bd189..e6b590b038 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -196,7 +196,9 @@ let subst_instance (_,subst,inst) =
       is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }
 
 let discharge_instance (_,inst) = 
-  { inst with is_class = Lib.discharge_global inst.is_class }
+  { inst with 
+      is_class = Lib.discharge_global inst.is_class;
+      is_impl = Lib.discharge_con inst.is_impl}
 
 let rebuild_instance inst = 
   match !(inst.is_global) with
-- 
cgit v1.2.3