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

13 files changed, 363 insertions, 187 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index acc764028..1f9f65b5c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -105,6 +105,7 @@ val label : kernel_name -> label
 val string_of_kn : kernel_name -> string
 val pr_kn : kernel_name -> Pp.std_ppcmds
 
+val kn_ord : kernel_name -> kernel_name -> int
 
 module KNset  : Set.S with type elt = kernel_name
 module KNpred : Predicate.S with type elt = kernel_name
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 68d928aef..2b29868bd 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -525,6 +525,24 @@ let process_module_bindings argids args =
     in
       List.iter2 process_arg argids args
 
+(* Same with module_type_body *)
+
+let rec seb2mse = function
+  | SEBident mp -> MSEident mp
+  | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
+  | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
+  | SEBwith (s,With_definition_body(l,cb)) ->
+      (match cb.const_body with
+	| Def c -> MSEwith(seb2mse s,With_Definition(l,Declarations.force c))
+	| _ -> assert false)
+  | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let process_module_seb_binding mbid seb =
+  process_module_bindings [id_of_mbid mbid]
+    [mbid,
+     (seb2mse seb,
+      { ann_inline = DefaultInline; ann_scope_subst = [] })]
+
 let intern_args interp_modtype (idl,(arg,ann)) =
   let inl = inline_annot ann in
   let lib_dir = Lib.library_dp() in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 21a7aeabe..9d44ba973 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -152,3 +152,7 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 (** For translator *)
 val process_module_bindings : module_ident list ->
   (mod_bound_id * (module_struct_entry annotated)) list -> unit
+
+(** For Printer *)
+val process_module_seb_binding :
+  mod_bound_id -> Declarations.struct_expr_body -> unit
diff --git a/library/libnames.ml b/library/libnames.ml
index 733c45af2..c82b3476e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -76,25 +76,37 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-(* outside of the kernel, names are ordered on their canonical part *)
+let global_ord_gen fc fmi x y =
+  let ind_ord (indx,ix) (indy,iy) =
+    let c = Pervasives.compare ix iy in
+    if c = 0 then kn_ord (fmi indx) (fmi indy) else c
+  in
+  match x, y with
+    | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
+    | IndRef indx, IndRef indy -> ind_ord indx indy
+    | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
+      let c = Pervasives.compare jx jy in
+      if c = 0 then ind_ord indx indy else c
+    | _, _ -> Pervasives.compare x y
+
+let global_ord_can = global_ord_gen canonical_con canonical_mind
+let global_ord_user = global_ord_gen user_con user_mind
+
+(* By default, [global_reference] are ordered on their canonical part *)
+
 module RefOrdered = struct
   type t = global_reference
-  let compare x y = 
-    let make_name = function
-      | ConstRef con -> 
-	  ConstRef(constant_of_kn(canonical_con con))
-      | IndRef (kn,i) ->
-	  IndRef(mind_of_kn(canonical_mind kn),i)
-      | ConstructRef ((kn,i),j )->
-	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
-      | VarRef id ->  VarRef id
-    in
-	Pervasives.compare (make_name x) (make_name y)
+  let compare = global_ord_can
 end
-  
+
+module RefOrdered_env = struct
+  type t = global_reference
+  let compare = global_ord_user
+end
+
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
-  
+
 (* Extended global references *)
 
 type syndef_name = kernel_name
@@ -103,6 +115,18 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
+(* We order [extended_global_reference] via their user part
+   (cf. pretty printer) *)
+
+module ExtRefOrdered = struct
+  type t = extended_global_reference
+  let compare x y =
+    match x, y with
+      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+      | SynDef knx, SynDef kny -> kn_ord knx kny
+      | _, _ -> Pervasives.compare x y
+end
+
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
diff --git a/library/libnames.mli b/library/libnames.mli
index 1f49b6a4f..18b6ac49a 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -51,7 +51,11 @@ module RefOrdered : sig
   type t = global_reference
   val compare : global_reference -> global_reference -> int
 end
-  
+
+module RefOrdered_env : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
 
 module Refset : Set.S with type elt = global_reference
 module Refmap : Map.S with type key = global_reference
@@ -64,6 +68,11 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SynDef of syndef_name
 
+module ExtRefOrdered : sig
+  type t = extended_global_reference
+  val compare : t -> t -> int
+end
+
 (** {6 Dirpaths } *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
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)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 87f11030e..4d35ac708 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -335,87 +335,11 @@ let assumptions_for_print lna =
 (*********************)
 (* *)
 
-let print_params env params =
-  if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
-
-let print_constructors envpar names types =
-  let pc =
-    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
-      (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
-  in
-  hv 0 (str "  " ++ pc)
-
-let build_inductive sp tyi =
-  let (mib,mip) = Global.lookup_inductive (sp,tyi) in
-  let params = mib.mind_params_ctxt in
-  let args = extended_rel_list 0 params in
-  let env = Global.env() in
-  let fullarity = match mip.mind_arity with
-    | Monomorphic ar -> ar.mind_user_arity
-    | Polymorphic ar ->
-	it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
-  let arity = hnf_prod_applist env fullarity args in
-  let cstrtypes = type_of_constructors env (sp,tyi) in
-  let cstrtypes =
-    Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
-  let cstrnames = mip.mind_consnames in
-  (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
-
-let print_one_inductive (sp,tyi) =
-  let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
-  let env = Global.env () in
-  let envpar = push_rel_context params env in
-  hov 0 (
-    pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++
-    str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
-  brk(0,2) ++ print_constructors envpar cstrnames cstrtypes
-
-let pr_mutual_inductive finite indl =
-  hov 0 (
-    str (if finite then "Inductive " else "CoInductive ") ++
-    prlist_with_sep (fun () -> fnl () ++ str"  with ")
-      print_one_inductive indl)
-
-let get_fields =
-  let rec prodec_rec l subst c =
-    match kind_of_term c with
-    | Prod (na,t,c) ->
-	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
-	prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
-    | LetIn (na,b,_,c) ->
-	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
-	prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
-    | _               -> List.rev l
-  in
-  prodec_rec [] []
-
-let pr_record (sp,tyi) =
-  let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
-  let env = Global.env () in
-  let envpar = push_rel_context params env in
-  let fields = get_fields cstrtypes.(0) in
-  hov 0 (
-    hov 0 (
-      str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++
-      print_params env params ++
-      str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
-      str ":= " ++ pr_id cstrnames.(0)) ++
-    brk(1,2) ++
-    hv 2 (str "{ " ++
-      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
-        (fun (id,b,c) ->
-	  pr_id id ++ str (if b then " : " else " := ") ++
-	  pr_lconstr_env envpar c) fields) ++ str" }")
-
 let gallina_print_inductive sp =
-  let (mib,mip) = Global.lookup_inductive (sp,0) in
+  let env = Global.env() in
+  let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
-  (if mib.mind_record & not !Flags.raw_print then
-    pr_record (List.hd names)
-  else
-    pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
+  pr_mutual_inductive_body env mib ++ fnl () ++
   with_line_skip
     (print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
@@ -606,11 +530,9 @@ let print_full_pure_context () =
           ++ str "." ++ fnl () ++ fnl ()
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta (mind_of_kn kn) in
-	  let (mib,mip) = Global.lookup_inductive (mind,0) in
-	  let mipv = mib.mind_packets in
-	  let names = list_tabulate (fun x -> (mind,x)) (Array.length mipv) in
-	  pr_mutual_inductive mib.mind_finite names ++ str "." ++
-	  fnl () ++ fnl ()
+	  let mib = Global.lookup_mind mind in
+	  pr_mutual_inductive_body (Global.env()) mib ++
+	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
 	  let (mp,_,l) = repr_kn kn in
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 3e05684c3..6d9c6ecc6 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -34,9 +34,6 @@ val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
   reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
 
-(** This function is exported for the graphical user-interface pcoq *)
-val build_inductive : mutual_inductive -> int ->
-  global_reference * rel_context * types * identifier array * types array
 val print_name : reference or_by_notation -> std_ppcmds
 val print_opaque_name : reference -> std_ppcmds
 val print_about : reference or_by_notation -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index f1f5d4c9f..d9b6d8082 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -539,3 +539,103 @@ let pr_instance_gmap insts =
   prlist_with_sep fnl (fun (gr, insts) ->
     prlist_with_sep fnl pr_instance (cmap_to_list insts))
     (Gmap.to_list insts)
+
+(** Inductive declarations *)
+
+open Declarations
+open Termops
+open Reduction
+open Inductive
+open Inductiveops
+
+let print_params env params =
+  if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
+
+let print_constructors envpar names types =
+  let pc =
+    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+      (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
+      (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
+  in
+  hv 0 (str "  " ++ pc)
+
+let build_ind_type env mip =
+  match mip.mind_arity with
+    | Monomorphic ar -> ar.mind_user_arity
+    | Polymorphic ar ->
+      it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
+
+let print_one_inductive env mib (mip,ind_typ) =
+  let params = mib.mind_params_ctxt in
+  (* In case of lets in params, mind_nparams <> List.length params *)
+  let lparams = List.length params in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env ind_typ args in
+  let envpar = push_rel_context params env in
+  let cstrtypes =
+    Array.map (fun c -> hnf_prod_applist envpar (lift lparams c) args)
+      mip.mind_user_lc
+  in
+  hov 0 (
+    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++
+    str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mib =
+  let mips = Array.to_list mib.mind_packets in
+  let ind_types = List.map (build_ind_type env) mips in
+  let mips_types = List.combine mips ind_types in
+  let ind_ctxt =
+    List.rev_map (fun (m,t) -> (Name m.mind_typename, None, t)) mips_types
+  in
+  let envind = push_rel_context ind_ctxt env in
+  hov 0 (
+    str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
+    prlist_with_sep (fun () -> fnl () ++ str"  with ")
+      (print_one_inductive envind mib) mips_types)
+
+let get_fields =
+  let rec prodec_rec l subst c =
+    match kind_of_term c with
+    | Prod (na,t,c) ->
+	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
+    | LetIn (na,b,_,c) ->
+	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
+    | _               -> List.rev l
+  in
+  prodec_rec [] []
+
+let print_record env mib =
+  let mip = mib.mind_packets.(0) in
+  let ind_typ = build_ind_type env mip in
+  let ind_name = mip.mind_typename in
+  let envind = push_rel_context [(Name ind_name, None, ind_typ)] env in
+  let params = mib.mind_params_ctxt in
+  let lparams = List.length params in
+  let args = extended_rel_list 0 params in
+  let arity = hnf_prod_applist env ind_typ args in
+  let envpar = push_rel_context params envind in
+  let cstr_typ =
+    hnf_prod_applist envpar (lift lparams mip.mind_user_lc.(0)) args
+  in
+  let fields = get_fields cstr_typ in
+  hov 0 (
+    hov 0 (
+      str "Record " ++ pr_id ind_name ++ brk(1,4) ++
+      print_params env params ++
+      str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
+      str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+    brk(1,2) ++
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+        (fun (id,b,c) ->
+	  pr_id id ++ str (if b then " : " else " := ") ++
+	  pr_lconstr_env envpar c) fields) ++ str" }")
+
+let pr_mutual_inductive_body env mib =
+  if mib.mind_record & not !Flags.raw_print then
+    print_record env mib
+  else
+    print_mutual_inductive env mib
diff --git a/parsing/printer.mli b/parsing/printer.mli
index ca91cfd4f..713484a76 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -143,3 +143,8 @@ val default_printer_pr : printer_pr
 
 val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
   Pp.std_ppcmds
+
+(** Inductive declarations *)
+
+val pr_mutual_inductive_body :
+  env -> Declarations.mutual_inductive_body -> std_ppcmds
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 9440a61bf..f258da587 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -12,6 +12,26 @@ open Names
 open Declarations
 open Nameops
 open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+    - The "short" one, that just prints the names of the fields.
+    - The "rich" one, that also tries to print the types of the fields.
+    The short version used to be the default behavior, but now we print
+    types by default. The following option allows to change this.
+    Technically, the environments in this file are either None in
+    the "short" mode or (Some env) in the "rich" one.
+*)
+
+let short = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "short module printing";
+      optkey   = ["Short";"Module";"Printing"];
+      optread  = (fun () -> !short) ;
+      optwrite = ((:=) short) }
 
 let get_new_id locals id =
   let rec get_id l id =
@@ -47,95 +67,141 @@ let print_kn locals kn =
 	with
 	    Not_found -> print_modpath locals kn
 
-let rec flatten_app mexpr l = match mexpr with
-  | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
-  | mexpr -> mexpr::l
+let nametab_register_dir mp =
+  let id = id_of_string "FAKETOP" in
+  let fp = Libnames.make_path empty_dirpath id in
+  let dir = make_dirpath [id] in
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
+  fp
 
-let rec print_module name locals with_body mb =
-  let body = match with_body, mb.mod_expr with
-    | false, _
-    | true, None -> mt()
-    | true, Some mexpr ->
-	spc () ++ str ":= " ++ print_modexpr locals mexpr
-  in
+(** Nota: the [global_reference] we register in the nametab below
+    might differ from internal ones, since we cannot recreate here
+    the canonical part of constant and inductive names, but only
+    the user names. This works nonetheless since we search now
+    [Nametab.the_globrevtab] modulo user name. *)
 
-  let modtype = 
-    match mb.mod_type with
-    | t -> spc () ++ str": " ++ 
-	print_modtype locals t
+let nametab_register_body mp fp (l,body) =
+  let push id ref =
+    Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
   in
-    hv 2 (str "Module " ++ name ++ modtype ++ body)
+  match body with
+    | SFBmodule _ -> () (* TODO *)
+    | SFBmodtype _ -> () (* TODO *)
+    | SFBconst _ ->
+      push (id_of_label l) (ConstRef (make_con mp empty_dirpath l))
+    | SFBmind mib ->
+      let mind = make_mind mp empty_dirpath l in
+      Array.iteri
+	(fun i mip ->
+	  push mip.mind_typename (IndRef (mind,i));
+	  Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1)))
+	    mip.mind_consnames)
+	mib.mind_packets
 
-and print_modtype locals mty =
+let print_body is_impl env mp (l,body) =
+  let name = str (string_of_label l) in
+  hov 2 (match body with
+    | SFBmodule _ -> str "Module " ++ name
+    | SFBmodtype _ -> str "Module Type " ++ name
+    | SFBconst cb ->
+      (match cb.const_body with
+	| Def _ -> str "Definition "
+	| OpaqueDef _ when is_impl -> str "Theorem "
+	| _ -> str "Parameter ") ++ name ++
+      (match env with
+	  | None -> mt ()
+	  | Some env ->
+	    str " :" ++ spc () ++
+	    hov 0 (Printer.pr_ltype_env env
+		     (Typeops.type_of_constant_type env cb.const_type)) ++
+	    (match cb.const_body with
+	      | Def l when is_impl ->
+		spc () ++
+		hov 2 (str ":= " ++
+		       Printer.pr_lconstr_env env (Declarations.force l))
+	      | _ -> mt ()) ++
+            str ".")
+    | SFBmind mib ->
+      try
+	let env = Option.get env in
+	Printer.pr_mutual_inductive_body env mib
+      with _ ->
+	(if mib.mind_finite then str "Inductive " else str "CoInductive")
+	++ name)
+
+let print_struct is_impl env mp struc =
+  begin
+    (* If [mp] is a globally visible module, we simply import it *)
+    try Declaremods.really_import_module mp
+    with _ ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+      let fp = nametab_register_dir mp in
+      List.iter (nametab_register_body mp fp) struc
+  end;
+  prlist_with_sep spc (print_body is_impl env mp) struc
+
+let rec flatten_app mexpr l = match mexpr with
+  | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l)
+  | SEBident mp -> mp::l
+  | _ -> assert false
+
+let rec print_modtype env mp locals mty =
   match mty with
     | SEBident kn -> print_kn locals kn
     | SEBfunctor (mbid,mtb1,mtb2) ->
-      (*    let env' = Modops.add_module (MPbid mbid)
-	    (Modops.body_of_type mtb) env
-	    in *)
-      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))
-	::locals in
-	hov 2 (str "Funsig" ++ spc () ++ str "(" ++
-		 pr_id (id_of_mbid mbid) ++ str " : " ++
-		 print_modtype locals mtb1.typ_expr ++
-		 str ")" ++ spc() ++ print_modtype locals' mtb2)
-  | SEBstruct (sign) -> 
-      hv 2 (str "Sig" ++ spc () ++ print_sig locals  sign ++ brk (1,-2) ++ str "End")
-  | SEBapply (mexpr,marg,_) ->
-      let lapp = flatten_app mexpr [marg] in
+      let mp1 = MPbound mbid in
+      let env' = Option.map
+	  (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
+      let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
+      in
+      (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+      hov 2 (str "Funsig" ++ spc () ++ str "(" ++
+	       pr_id (id_of_mbid mbid) ++ str ":" ++
+	       print_modtype env mp1 locals seb1 ++
+	       str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
+  | SEBstruct (sign) ->
+      let env' = Option.map
+	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+      hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
+	    brk (1,-2) ++ str "End")
+  | SEBapply _ ->
+      let lapp = flatten_app mty [] in
       let fapp = List.hd lapp in
       let mapp = List.tl lapp in
-	hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++
-		 prlist_with_sep spc (print_modexpr locals) mapp ++ str")")
+      hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
+		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
   | SEBwith(seb,With_definition_body(idl,cb))->
+      let env' = None in (* TODO: build a proper environment if env <> None *)
       let s = (String.concat "." (List.map string_of_id idl)) in
-      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
+      hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
   | SEBwith(seb,With_module_body(idl,mp))->
       let s =(String.concat "." (List.map string_of_id idl)) in
-      hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++
+      hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
 
-and print_sig locals sign = 
-  let print_spec (l,spec) = str (match spec with
-    | SFBconst cb ->
-      (match cb.const_body with
-	| Def _ -> "Definition "
-	| Undef _ | OpaqueDef _ -> "Parameter ")
-    | SFBmind _ -> "Inductive "
-    | SFBmodule _ -> "Module "
-    | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l)
-  in
-    prlist_with_sep spc print_spec sign
-
-and print_struct locals struc = 
-  let print_body (l,body) = str (match body with
-    | SFBconst cb ->
-      (match cb.const_body with
-	| Undef _ -> "Parameter "
-	| Def _ -> "Definition "
-	| OpaqueDef _ -> "Theorem ")
-    | SFBmind _ -> "Inductive "
-    | SFBmodule _ -> "Module "
-    | SFBmodtype _ -> "Module Type ") ++ str (string_of_label l)
-  in
-    prlist_with_sep spc print_body struc
-
-and print_modexpr locals mexpr = match mexpr with
+let rec print_modexpr env mp locals mexpr = match mexpr with
   | SEBident mp -> print_modpath locals mp
   | SEBfunctor (mbid,mty,mexpr) ->
-(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env
-      in *)
+      let mp' = MPbound mbid in
+      let env' = Option.map
+	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
+      let typ = Option.default mty.typ_expr mty.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
+      (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
       hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
-	     str ":" ++ print_modtype locals mty.typ_expr ++
-      str ")" ++ spc () ++ print_modexpr locals' mexpr)
-  | SEBstruct ( struc) -> 
-      hv 2 (str "Struct" ++ spc () ++ print_struct locals struc ++ brk (1,-2) ++ str "End")
-  | SEBapply (mexpr,marg,_) ->
-      let lapp = flatten_app mexpr [marg] in
-	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
-  | SEBwith (_,_)-> anomaly "Not avaible yet"
+	     str ":" ++ print_modtype env mp' locals typ ++
+      str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
+  | SEBstruct struc ->
+      let env' = Option.map
+	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+      hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
+	    brk (1,-2) ++ str "End")
+  | SEBapply _ ->
+      let lapp = flatten_app mexpr [] in
+      hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | SEBwith (_,_)-> anomaly "Not available yet"
 
 
 let rec printable_body dir =
@@ -149,13 +215,42 @@ let rec printable_body dir =
     with
 	Not_found -> true
 
+(** Since we might play with nametab above, we should reset to prior
+    state after the printing *)
 
-let print_module with_body mp =
+let print_modexpr' env mp mexpr =
+  States.with_state_protection (print_modexpr env mp []) mexpr
+let print_modtype' env mp mty =
+  States.with_state_protection (print_modtype env mp []) mty
+
+let print_module' env mp with_body mb =
   let name = print_modpath [] mp in
-    print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
+  let body = match with_body, mb.mod_expr with
+    | false, _
+    | true, None -> mt()
+    | true, Some mexpr ->
+	spc () ++ str ":= " ++ print_modexpr' env mp mexpr
+  in
+  let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type
+  in
+  hv 0 (str "Module " ++ name ++ modtype ++ body)
+
+exception ShortPrinting
+
+let print_module with_body mp =
+  let me = Global.lookup_module mp in
+  try
+    if !short then raise ShortPrinting;
+    print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
+  with _ ->
+    print_module' None mp with_body me ++ fnl ()
 
 let print_modtype kn =
   let mtb = Global.lookup_modtype kn in
   let name = print_kn [] kn in
-      str "Module Type " ++ name ++ str " = " ++
-	print_modtype [] mtb.typ_expr ++ fnl ()
+  str "Module Type " ++ name ++ str " = " ++
+  (try
+     if !short then raise ShortPrinting;
+     print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+   with _ ->
+     print_modtype' None kn mtb.typ_expr)
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] *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a9e390538..51fd69149 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -199,9 +199,14 @@ let print_modtype r =
   let (loc,qid) = qualid_of_reference r in
   try
     let kn = Nametab.locate_modtype qid in
-      msgnl (Printmod.print_modtype kn)
-  with
-      Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid)
+    msgnl (Printmod.print_modtype kn)
+  with Not_found ->
+    (* Is there a module of this name ? If yes we display its type *)
+    try
+      let mp = Nametab.locate_module qid in
+      msgnl (Printmod.print_module false mp)
+    with Not_found ->
+      msgnl (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let dump_universes_gen g s =
   let output = open_out s in