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

1 files changed, 4 insertions, 5 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 725a70559..ad5424deb 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -19,12 +19,11 @@ open Util
 open Pp
 open Miniml
 
-(** Sets and maps for [global_reference] that do _not_ work modulo
-    name equivalence (otherwise use Refset / Refmap ) *)
+(** Sets and maps for [global_reference] that use the "user" [kernel_name]
+    instead of the canonical one *)
 
-module RefOrd = struct type t = global_reference let compare = compare end
-module Refmap' = Map.Make(RefOrd)
-module Refset' = Set.Make(RefOrd)
+module Refmap' = Map.Make(RefOrdered_env)
+module Refset' = Set.Make(RefOrdered_env)
 
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)