From fa87b9196df910caa4cb085f9dee69ca58df0c34 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 6 Aug 2009 19:20:38 +0000
Subject: Cleaning of Nametab continued + fixed a compilation bug in previous
 commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/libnames.ml           |  6 +++---
 library/nametab.ml            |  2 +-
 library/nametab.mli           | 24 ++++++++++++++++++------
 plugins/extraction/table.ml   |  2 +-
 plugins/interface/centaur.ml4 |  2 +-
 5 files changed, 24 insertions(+), 12 deletions(-)

diff --git a/library/libnames.ml b/library/libnames.ml
index 650b5c33f..21be8f7d1 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -188,7 +188,7 @@ let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
 
 let decode_kn kn = 
-  let rec dir_of_mp = function
+  let rec dirpath_of_module = function
     | MPfile dir -> repr_dirpath dir
     | MPbound mbid -> 
 	let _,_,dp = repr_mbid mbid in
@@ -198,11 +198,11 @@ let decode_kn kn =
 	let _,_,dp = repr_msid msid in
 	let id = id_of_msid msid in
 	  id::(repr_dirpath dp) 
-    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+    | MPdot(mp,l) -> (id_of_label l)::(dirpath_of_module mp)
   in
   let mp,sec_dir,l = repr_kn kn in
     if (repr_dirpath sec_dir) = [] then
-     (make_dirpath (dir_of_mp mp)),id_of_label l
+     (make_dirpath (dirpath_of_module mp)),id_of_label l
     else
       anomaly "Section part should be empty!"
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 7f148f0d3..a511a4e60 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -460,7 +460,7 @@ let basename_of_global ref =
 let path_of_syndef kn = 
   Globrevtab.find (SynDef kn) !the_globrevtab
 
-let dir_of_mp mp =
+let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
 
 
diff --git a/library/nametab.mli b/library/nametab.mli
index c529120dd..634e4d034 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -16,7 +16,21 @@ open Libnames
 (*i*)
 
 (*s This module contains the tables for globalization, which
-    associates internal object references to qualified names (qualid). *)
+    associates internal object references to qualified names (qualid).
+
+    There are three classes of names:
+
+    1a- internal kernel names: [kernel_name], [constant], [inductive],
+        [module_path]
+
+    1b- other internal names: [global_reference], [syndef_name],
+        [extended_global_reference], [global_dir_reference], ...
+
+    2- full, non ambiguous user names: [full_path] and [dir_path]
+
+    3- non necessarily full, possibly ambiguous user names: [reference]
+       and [qualid]
+*)
 
 (* Most functions in this module fall into one of the following categories:
    \begin{itemize}
@@ -130,14 +144,12 @@ val full_name_module : qualid -> dir_path
 (*s Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
-(* Returns the dirpath associated to a module path *)
-
-val dir_of_mp : module_path -> dir_path
-
-(* Returns full path bound to a global reference or syntactic definition *)
+(* Returns the full path bound to a global reference or syntactic
+   definition, and the (full) dirpath associated to a module path *)
 
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
+val dirpath_of_module : module_path -> dir_path
 
 (* Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 13a730ac2..e6d634466 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -204,7 +204,7 @@ let safe_pr_long_global r =
     | _ -> assert false
 
 let pr_long_mp mp =
-  let lid = repr_dirpath (Nametab.dir_of_mp mp) in
+  let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
   str (String.concat "." (List.map string_of_id (List.rev lid)))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index c8fc7bdf3..ee46cef8b 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -146,7 +146,7 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, !current_goal_index
     else
       (0, 0)
-  and statnum = Lib.current_state_label ()
+  and statnum = Lib.current_command_label ()
   and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
   and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
    (ctf_header "acknowledge" request_id ++
-- 
cgit v1.2.3