From 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 19 Sep 1999 14:17:35 +0000
Subject:  - un effort sur la doc (ocamlweb)  - module Nametab  - module
 Impargs  - correction bug : Parameter id : t => vérification que t est bien
 un type
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/nametab.mli | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100755 library/nametab.mli

(limited to 'library/nametab.mli')

diff --git a/library/nametab.mli b/library/nametab.mli
new file mode 100755
index 000000000..2d0cd62eb
--- /dev/null
+++ b/library/nametab.mli
@@ -0,0 +1,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
+
-- 
cgit v1.2.3