From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 27 Mar 2018 02:37:19 +0200 Subject: Swapping Context and Constr: defining declarations on constr in Constr. This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). --- pretyping/typeclasses.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4a56960c..80c6d8239 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -35,10 +35,10 @@ type typeclass = { (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if -- cgit v1.2.3