Keys (coq-core.Keys)

type key

val declare_equiv_keys : key -> key -> unit

Declare two keys as being equivalent.

val equiv_keys : key -> key -> bool

Check equivalence of keys.

val constr_key : 
  ( 'a -> ( 'a, 't, 'u, 'i ) Constr.kind_of_term ) ->
  'a ->
  key option

Compute the head key of a term.

val pr_keys : ( Names.GlobRef.t -> Pp.t ) -> Pp.t

Pretty-print the mapping