diff options
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r-- | vernac/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 415b98f2d..c3300a361 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -166,8 +166,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum c' in let ctx'' = ctx' @ ctx in - let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in - let cl, u = Typeclasses.typeclass_univ_instance k in + let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in + let u = EConstr.EInstance.kind !evars u in + let cl, u = Typeclasses.typeclass_univ_instance (k, u) in let _, args = List.fold_right (fun decl (args, args') -> match decl with |