aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a528b9640..d6d4b164b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
let ctx'' = ctx' @ ctx 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 cl = Typeclasses.typeclass_univ_instance (k, u) in
let _, args =
List.fold_right (fun decl (args, args') ->
match decl with