CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"

8 files changed, 37 insertions, 31 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 5933649da..f87e76dd1 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -6,6 +6,11 @@ We renamed the following functions:
 
   Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
   Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
+  Printer.pr_var_list_decl       -> Printer.pr_compacted_decl
+
+We renamed the following modules:
+
+  Context.ListNamed -> Context.Compacted
 
 The following type aliases where removed
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 3f36059dd..1c2d261e5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -17,7 +17,7 @@ open Environ
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module NamedListDecl = Context.NamedList.Declaration
+module CompactedDecl = Context.Compacted.Declaration
 
 (* Sorts and sort family *)
 
@@ -986,21 +986,21 @@ let compact_named_context_reverse sign =
   let compact l decl =
     match decl, l with
     | NamedDecl.LocalAssum (i,t), [] ->
-       [NamedListDecl.LocalAssum ([i],t)]
+       [CompactedDecl.LocalAssum ([i],t)]
     | NamedDecl.LocalDef (i,c,t), [] ->
-       [NamedListDecl.LocalDef ([i],c,t)]
-    | NamedDecl.LocalAssum (i1,t1), NamedListDecl.LocalAssum (li,t2) :: q ->
+       [CompactedDecl.LocalDef ([i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
        if Constr.equal t1 t2
-       then NamedListDecl.LocalAssum (i1::li, t2) :: q
-       else NamedListDecl.LocalAssum ([i1],t1) :: NamedListDecl.LocalAssum (li,t2) :: q
-    | NamedDecl.LocalDef (i1,c1,t1), NamedListDecl.LocalDef (li,c2,t2) :: q ->
+       then CompactedDecl.LocalAssum (i1::li, t2) :: q
+       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
        if Constr.equal c1 c2 && Constr.equal t1 t2
-       then NamedListDecl.LocalDef (i1::li, c2, t2) :: q
-       else NamedListDecl.LocalDef ([i1],c1,t1) :: NamedListDecl.LocalDef (li,c2,t2) :: q
+       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
+       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
     | NamedDecl.LocalAssum (i,t), q ->
-       NamedListDecl.LocalAssum ([i],t) :: q
+       CompactedDecl.LocalAssum ([i],t) :: q
     | NamedDecl.LocalDef (i,c,t), q ->
-       NamedListDecl.LocalDef ([i],c,t) :: q
+       CompactedDecl.LocalDef ([i],c,t) :: q
   in
   Context.Named.fold_inside compact ~init:[] sign
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 5d85088f8..bfd902f44 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -238,8 +238,8 @@ val fold_named_context_both_sides :
   ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
     Context.Named.t -> init:'a -> 'a
 val mem_named_context : Id.t -> Context.Named.t -> bool
-val compact_named_context : Context.Named.t -> Context.NamedList.t
-val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t
+val compact_named_context : Context.Named.t -> Context.Compacted.t
+val compact_named_context_reverse : Context.Named.t -> Context.Compacted.t
 
 val clear_named_body : Id.t -> env -> env
 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 36d676f5d..8ef7a0554 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -15,6 +15,7 @@ open Printer
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
+module CompactedDecl = Context.Compacted.Declaration
 
 (** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
@@ -194,12 +195,12 @@ let process_goal sigma g =
     Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
   in
   let process_hyp d (env,l) =
-    let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
-    let d' = Context.NamedList.Declaration.to_named_context d in
+    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in
+    let d' = CompactedDecl.to_named_context d in
       (List.fold_right Environ.push_named d' env,
-       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
   let (_env, hyps) =
-    Context.NamedList.fold process_hyp
+    Context.Compacted.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
diff --git a/kernel/context.ml b/kernel/context.ml
index fed6a5feb..47e0a08e5 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -412,7 +412,7 @@ struct
     List.map_filter filter
 end
 
-module NamedList =
+module Compacted =
   struct
     module Declaration =
       struct
diff --git a/kernel/context.mli b/kernel/context.mli
index 72fbfb540..366f0ffc1 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -251,7 +251,7 @@ sig
   val to_instance : t -> Constr.t list
 end
 
-module NamedList :
+module Compacted :
 sig
   module Declaration :
   sig
diff --git a/printing/printer.ml b/printing/printer.ml
index 5c62c2af0..e3f4ea999 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -24,7 +24,7 @@ open Declarations
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module NamedListDecl = Context.NamedList.Declaration
+module CompactedDecl = Context.Compacted.Declaration
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
@@ -252,11 +252,11 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
-let pr_var_list_decl env sigma decl =
+let pr_compacted_decl env sigma decl =
   let ids, pbody, typ = match decl with
-    | NamedListDecl.LocalAssum (ids, typ) ->
+    | CompactedDecl.LocalAssum (ids, typ) ->
        ids, mt (), typ
-    | NamedListDecl.LocalDef (ids,c,typ) ->
+    | CompactedDecl.LocalDef (ids,c,typ) ->
        (* Force evaluation *)
        let pb = pr_lconstr_env env sigma c in
        let pb = if isCast c then surround pb else pb in
@@ -270,11 +270,11 @@ let pr_var_list_decl env sigma decl =
 let pr_var_decl env sigma decl =
   let decl = match decl with
     | NamedDecl.LocalAssum (id, t) ->
-       NamedListDecl.LocalAssum ([id], t)
+       CompactedDecl.LocalAssum ([id], t)
     | NamedDecl.LocalDef (id,c,t) ->
-       NamedListDecl.LocalDef ([id],c,t)
+       CompactedDecl.LocalDef ([id],c,t)
   in
-  pr_var_list_decl env sigma decl
+  pr_compacted_decl env sigma decl
 
 let pr_rel_decl env sigma decl =
   let na = RelDecl.get_name decl in
@@ -316,9 +316,9 @@ let pr_rel_context_of env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env sigma =
   let sign_env =
-    Context.NamedList.fold
+    Context.Compacted.fold
       (fun d pps ->
-         let pidt =  pr_var_list_decl env sigma d in
+         let pidt =  pr_compacted_decl env sigma d in
          (pps ++ fnl () ++ pidt))
       (Termops.compact_named_context (named_context env)) ~init:(mt ())
   in
@@ -343,12 +343,12 @@ let pr_context_limit n env sigma =
   else
     let k = lgsign-n in
     let _,sign_env =
-      Context.NamedList.fold
+      Context.Compacted.fold
         (fun d (i,pps) ->
            if i < k then
 	     (i+1, (pps ++str "."))
 	   else
-             let pidt = pr_var_list_decl env sigma d in
+             let pidt = pr_compacted_decl env sigma d in
 	     (i+1, (pps ++ fnl () ++
 		      str (emacs_str "") ++
 		      pidt)))
diff --git a/printing/printer.mli b/printing/printer.mli
index 695ab33b2..196f7cb54 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -109,7 +109,7 @@ val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
 
 val pr_var_decl            : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
-val pr_var_list_decl       : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds
 val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
 
 val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds