Merge branch 'v8.5'

3 files changed, 11 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 982d9bfe39..8c56d0ccfe 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for =
 	      let (argscs,_) = find_remaining_scopes pats [] g in
 	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
 	| NApp (NRef g,args) ->
-	      ensure_kind top loc g;
+	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
 	      let pats1,pats2 = List.chop nvars pats in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e304725d46..87f7a6d6e4 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -245,21 +245,21 @@ let combine_params_freevar =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l
-    | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
+    | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let (loc, r, _ as clapp) = destClassAppExpl ty in
+      let (_, r, _, _ as clapp) = destClassAppExpl ty in
       let (loc, qid) = qualid_of_reference r in
       let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -267,7 +267,7 @@ let implicit_application env ?(allow_partial=true) f ty =
   in
     match is_class with
     | None -> ty, env
-    | Some ((loc, id, par), gr) ->
+    | Some ((loc, id, par, inst), gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
@@ -285,7 +285,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    CAppExpl (loc, (None, id, None), args), avoid
+	    CAppExpl (loc, (None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 818f7e9a86..a3721af660 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Globnames
 val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
-val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)