diff options
| -rw-r--r-- | library/libnames.ml | 6 | ||||
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rwxr-xr-x | library/nametab.mli | 24 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 2 | ||||
| -rw-r--r-- | 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 ++ |