diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 638cc4304e..4d28ee55b1 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -41,6 +41,15 @@ val find_projection_nparams : global_reference -> int (* raise [Not_found] if not a projection *) val find_projection : global_reference -> struc_typ +(* we keep an index (dnet) of record's arguments + fields + (=methods). Here is how to declare them: *) +val declare_method : + global_reference -> Evd.evar -> Evd.evar_map -> unit + (* and here is how to search for methods matched by a given term: *) +val methods_matching : constr -> + ((global_reference*Evd.evar*Evd.evar_map) * + (constr*existential_key)*Termops.subst) list + (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) (* structure *) |