From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- interp/implicit_quantifiers.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e304725d..87f7a6d6 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 = -- cgit v1.2.3