aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/classes.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b513f2e2e8..2f1b7138bd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -171,6 +171,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
+ evars := mark_resolvables !evars;
evars := resolve_typeclasses env !evars;
let sigma = !evars in
let subst = List.map (Evarutil.nf_evar sigma) subst in