Pushing Pierre's factorization of names in goal context printing from

coqide to coqtop.

(Joint work with Pierre)

2 files changed, 6 insertions, 2 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 5cb964b9cf..6b5a6cdb9a 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -87,7 +87,7 @@ let rel_context_tags ctx =
     goal assumptions. *)
 
 type named_context = named_declaration list
-type compacted_named_context = named_list_declaration list
+type named_list_context = named_list_declaration list
 
 let empty_named_context = []
 
@@ -112,6 +112,7 @@ let instance_from_named_context sign =
   List.map_filter filter sign
 
 let fold_named_context f l ~init = List.fold_right f l init
+let fold_named_list_context f l ~init = List.fold_right f l init
 let fold_named_context_reverse f ~init l = List.fold_left f init l
 
 (*s Signatures of ordered section variables *)
diff --git a/kernel/context.mli b/kernel/context.mli
index b7eb7a76a3..e1ff708e7b 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -54,7 +54,7 @@ val eq_rel_declaration :
 
 type named_context = named_declaration list
 type section_context = named_context
-type compacted_named_context = named_list_declaration list
+type named_list_context = named_list_declaration list
 type rel_context = rel_declaration list
 (** In [rel_context], more recent declaration is on top *)
 
@@ -74,6 +74,9 @@ val named_context_equal : named_context -> named_context -> bool
 val fold_named_context :
   (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
 
+val fold_named_list_context :
+  (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
+
 (** newer declarations first *)
 val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a