[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.

2 files changed, 6 insertions, 5 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2e213a51d..fc266849d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -442,19 +442,20 @@ let add_class cl =
 
 let instance_constructor (cl,u) args =
   let lenpars = List.count is_local_assum (snd cl.cl_context) in
+  let open EConstr in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> 
         let ind = ind, u in
-          (Some (applistc (mkConstructUi (ind, 1)) args),
-	   applistc (mkIndU ind) pars)
+          (Some (applist (mkConstructUi (ind, 1), args)),
+           applist (mkIndU ind, pars))
       | ConstRef cst -> 
         let cst = cst, u in
 	let term = match args with
 	  | [] -> None
 	  | _ -> Some (List.last args)
 	in
-	  (term, applistc (mkConstU cst) pars)
+          (term, applist (mkConstU cst, pars))
       | _ -> assert false
 
 let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 618826f3d..8ee061330 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