diff options
| -rw-r--r-- | interp/implicit_quantifiers.ml | 16 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 4 |
2 files changed, 10 insertions, 10 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e304725d4..87f7a6d6e 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 818f7e9a8..a3721af66 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 *) |