diff options
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r-- | pretyping/recordops.ml | 44 |
1 files changed, 0 insertions, 44 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5aced6e10..eaf7bf0aa 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -105,50 +105,6 @@ let find_projection = function | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found -(* Management of a field store : each field + argument of the inferred - * records are stored in a discrimination tree *) - -let subst_id s (gr,ev,evm) = - (fst(subst_global s gr),ev,Evd.subst_evar_map s evm) - -module MethodsDnet : Term_dnet.S - with type ident = global_reference * Evd.evar * Evd.evar_map - = Term_dnet.Make - (struct - type t = global_reference * Evd.evar * Evd.evar_map - (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to - do w.r.t. evar maps. *) - let compare = Pervasives.compare - let subst = subst_id - let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev) - end) - (struct - let reduce c = Reductionops.head_unfold_under_prod - Names.full_transparent_state (Global.env()) Evd.empty c - let direction = true - end) - -let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state" - -open Libobject - -let load_method (_,(ty,id)) = - meth_dnet := MethodsDnet.add ty id !meth_dnet - -let in_method : constr * MethodsDnet.ident -> obj = - declare_object - { (default_object "RECMETHODS") with - load_function = (fun _ -> load_method); - cache_function = load_method; - subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); - classify_function = (fun x -> Substitute x) - } - -let methods_matching c = MethodsDnet.search_pattern !meth_dnet c - -let declare_method cons ev sign = - Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign))) - (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) |