5 files changed, 71 insertions, 19 deletions

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)