diff options
Diffstat (limited to 'contrib/subtac/subtac_classes.ml')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 48 |
1 files changed, 15 insertions, 33 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 56bd40d30..7b8d982d1 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -92,45 +92,27 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in - let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in let tclass = match bk with - | Implicit -> - let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in - let k = class_info (Nametab.global id) in - let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in - let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 (fst k.cl_context) in - if needlen <> applen then - Classes.mismatched_params env (List.map fst par) (snd k.cl_context); - let (ci, rd) = k.cl_context in - let pars = List.rev (List.combine ci rd) in - let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) - (fun avoid (clname, (id, _, t)) -> - match clname with - Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *) - else CHole (Util.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - par pars - in Topconstr.CAppExpl (loc, (None, id), pars) - + | Implicit -> + Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) + ~allow_partial:false (fun avoid (clname, (id, _, t)) -> + match clname with + | Some (cl, b) -> + let t = + if b then + let _k = class_info cl in + CHole (Util.dummy_loc, Some Evd.InternalHole) + else CHole (Util.dummy_loc, None) + in t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + cl | Explicit -> cl in - let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in - let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in - let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in - on_free_vars (List.rev (gen_ids @ fvs)); - let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in - let ctx, avoid = Classes.name_typeclass_binders bound ctx in - let ctx = List.append ctx (List.rev gen_ctx) in + let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in |