summaryrefslogtreecommitdiff
path: root/contrib/subtac/context.mli
blob: 671d6f3619266da9c38fd4b2b60d9e4571904106 (plain)
1
2
3
4
5
type t = Term.rel_declaration list
val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c
val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c
val id_of_name : Names.name -> Names.identifier
val subst_env : 'a -> 'b -> 'a * 'b