aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/typeclasses.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bf346bd18..e6b590b03 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