diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index b38a249b73..a464eab127 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -58,13 +58,7 @@ let is_local_for_hint i = let add_instance_base inst = let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality - inst.is_info; - List.iter (fun (path, pri, c) -> - let h = Hints.IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in - add_instance_hint h path - ~locality pri) - (build_subclasses ~check:(not (isVarRef inst.is_impl)) - (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) + inst.is_info let mk_instance cl info glob impl = let global = @@ -161,8 +155,17 @@ let subst_class (subst,cl) = let do_subst_context (grs,ctx) = List.Smart.map (Option.Smart.map do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> - (x, y, Option.Smart.map do_subst_con z)) projs in + let do_subst_meth m = + let c = Option.Smart.map do_subst_con m.meth_const in + if c == m.meth_const then m + else + { + meth_name = m.meth_name; + meth_info = m.meth_info; + meth_const = c; + } + in + let do_subst_projs projs = List.Smart.map do_subst_meth projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; @@ -247,10 +250,10 @@ let add_class cl = let add_class env sigma cl = add_class cl; - List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with + List.iter (fun m -> + match m.meth_info with + | Some info -> + (match m.meth_const with | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance ~warn:true env sigma (Some info) false (GlobRef.ConstRef b)) | _ -> ()) @@ -430,9 +433,9 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = let rest' = List.filter (fun v -> not (is_id v)) rest in let {CAst.loc;v=mid} = get_id loc_mid in - List.iter (fun (n, _, x) -> - if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) x) k.cl_projs; + List.iter (fun m -> + if Name.equal m.meth_name (Name mid) then + Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) m.meth_const) k.cl_projs; c :: props, rest' with Not_found -> ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest |