diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 22:49:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 (patch) | |
| tree | 0fd697ed68507449268811a630a201f7637c3553 /vernac/classes.ml | |
| parent | 9938aed874d3e15e5d21689ea841bdc3e6ebb40e (diff) | |
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.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
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 |