From 7799626c67c39c6bd2c5faf247456efb2c26ae82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Dec 2017 04:34:45 +0100
Subject: [econstr] Cleanup in `vernac/classes.ml`.

We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.

Thanks to @SkySkimmer for lots of comments and bug-finding.
---
 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 618826f3d0..8ee061330a 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -83,8 +83,8 @@ val is_instance : global_reference -> bool
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
-val instance_constructor : typeclass Univ.puniverses -> constr list ->
-  constr option * types
+val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list ->
+  EConstr.t option * EConstr.t
 
 (** Filter which evars to consider for resolution. *)
 type evar_filter = Evar.t -> Evar_kinds.t -> bool
-- 
cgit v1.2.3