From 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 22:49:32 +0200 Subject: Make the typeclass implementation fully compatible with universe polymorphism. This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') 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 -- cgit v1.2.3