aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-11 15:36:18 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-11 15:36:18 +0000
commit7cde682014e0dd179ae3bed029a07c8bf0c71157 (patch)
tree55a5928dc7cd035700275fcfcb41c8221027db37 /library/nametab.ml
parentb3ebb256717364d6d6ed631cd7830e46a8ab6863 (diff)
Print Module (Type) M now tries to print more details
"Print Module M" prints now by default both a signature (fields with their types) and a body (fields with their types and transparent bodies). "Print Module Type M" could be used both when M is a module or a module Type, it will only display th signature of M. The earlier minimalist behavior (printing only the field names) could be reactivated by option "Set Short Module Printing". For the moment, the content of internal sub-modules and sub-modtypes are not displayed. Note: this commit is an experiment, many sitations are still unsupported. When such situations are encountered, Print Module will fall back on the earlier minimalist behavior. This might occur in particular in presence of "with" annotations, or in the conjonction of a non-global module (i.e. functor or module type) and internal sub-modules. Side effects of this commit: - a better compare function for global_reference, with no allocations at each comparison - Nametab.the_globrevtab is now searched according to user part only of a kernel_name - The printing of an inductive block is now in Printer, and rely less on the Nametab. Instead, we use identifiers in mind_typename and mind_consnames. Note that Print M.indu will not display anymore the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rw-r--r--library/nametab.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/library/nametab.ml b/library/nametab.ml
index e43ae650c..c6f04b016 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -287,10 +287,7 @@ let the_dirtab = ref (DirTab.empty : dirtab)
(* Reversed name tables ***************************************************)
(* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(struct
- type t=extended_global_reference
- let compare = compare
- end)
+module Globrevtab = Map.Make(ExtRefOrdered)
type globrevtab = full_path Globrevtab.t
let the_globrevtab = ref (Globrevtab.empty : globrevtab)