diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 19:11:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (patch) | |
| tree | fbe0e3ae6901faba4f14b8cd4dbda019ce9a7829 /pretyping/typeclasses.ml | |
| parent | b8a7222e670f69e024d50394afd88204e15d1b29 (diff) | |
Safe API for accessing universe constraints of global references.
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 201f79c39..bae831b63 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) | IndRef c -> let mib,oib = Global.lookup_inductive c in - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') |