diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-03 16:09:03 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-03 20:05:57 +0200 |
commit | 267c880c5e8b73770316518a2a820e779c121fdb (patch) | |
tree | ff853a754928a323fe88a1843cf1e065fa2088cb /library/nametab.mli | |
parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) |
Exporting Nametab generic API.
Diffstat (limited to 'library/nametab.mli')
-rw-r--r-- | library/nametab.mli | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index d20c399b6..3d90e1b5a 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -173,3 +173,36 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid val extended_locate : qualid -> extended_global_reference (*= locate_extended *) val absolute_reference : full_path -> global_reference (** = global_of_path *) + +(** Generic name handling *) + +module type UserName = sig + type t + val equal : t -> t -> bool + val to_string : t -> string + val repr : t -> Id.t * module_ident list +end + +module type EqualityType = +sig + type t + val equal : t -> t -> bool +end + +module type NAMETREE = sig + type elt + type t + type user_name + + val empty : t + val push : visibility -> user_name -> elt -> t -> t + val locate : qualid -> t -> elt + val find : user_name -> t -> elt + val exists : user_name -> t -> bool + val user_name : qualid -> t -> user_name + val shortest_qualid : Id.Set.t -> user_name -> t -> qualid + val find_prefixes : qualid -> t -> elt list +end + +module Make (U : UserName) (E : EqualityType) : + NAMETREE with type user_name = U.t and type elt = E.t |