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.
---
 pretyping/typeclasses.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8e90ca17d..99cdbd3a36 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,10 @@ type direction = Forward | Backward
 
 (** This module defines type-classes *)
 type typeclass = {
+  (** The toplevel universe quantification in which the typeclass lives. In
+      particular, [cl_props] and [cl_context] are quantified over it. *)
+  cl_univs : Univ.AUContext.t;
+
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference;
@@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list
 
 (** Get the instantiated typeclass structure for a given universe instance. *)
-val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
+val typeclass_univ_instance : typeclass puniverses -> typeclass
 
 (** Just return None if not a class *)
 val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
-- 
cgit v1.2.3