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

(* $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

val rollback : ('a -> 'b) -> 'a -> 'b