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

1 files changed, 4 insertions, 3 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 []