diff options
| author | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-29 12:12:35 +0200 |
| commit | e76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (patch) | |
| tree | 5bcdbed2dac27feeb27caf840e8cad24e7483a9a /interp/implicit_quantifiers.ml | |
| parent | aff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff) | |
| parent | 0dac9618c695a345f82ee302b205217fff29be29 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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 = |