aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.mli
blob: 463dc63de1b7a8b17624ee969460474e31b6095a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14

(* $Id$ *)

(*i*)
open Names
(*i*)

(* This module contains the table for globalization, which associates global
   names (section paths) to identifiers. *)

val push : identifier -> section_path -> unit

val sp_of_id : path_kind -> identifier -> section_path
val fw_sp_of_id : identifier -> section_path