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

coqide to coqtop.

(Joint work with Pierre)

6 files changed, 28 insertions, 21 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 1df9d0fc3..a91be2aa4 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -168,16 +168,6 @@ let concl_next_tac sigma concl =
     "right"
   ])
 
-let compact_named_context c =
-  let compact l (i1,c1,t1) =
-    match l with
-    | [] -> [[i1],c1,t1]
-    | (l2,c2,t2)::q ->
-       if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-       then (i1::l2,c2,t2)::q
-       else ([i1],c1,t1)::l
-  in Context.fold_named_context_reverse compact ~init:[] c
-
 let process_goal sigma g =
   let env = Goal.V82.env sigma g in
   let min_env = Environ.reset_context env in
@@ -189,7 +179,8 @@ let process_goal sigma g =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
     (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
   let hyps =
-    List.map process_hyp (compact_named_context (Environ.named_context env)) in
+    List.map process_hyp
+      (Termops.compact_named_context (Environ.named_context env)) in
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let goals () =
diff --git a/kernel/context.ml b/kernel/context.ml
index 5cb964b9c..6b5a6cdb9 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 b7eb7a76a..e1ff708e7 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
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5813cd416..a1f1f52ff 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -940,6 +940,16 @@ let rec mem_named_context id = function
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
+let compact_named_context sign =
+  let compact l (i1,c1,t1) =
+    match l with
+    | [] -> [[i1],c1,t1]
+    | (l2,c2,t2)::q ->
+       if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
+       then (i1::l2,c2,t2)::q
+       else ([i1],c1,t1)::l
+  in Context.fold_named_context_reverse compact ~init:[] sign
+
 let clear_named_body id env =
   let aux _ = function
   | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 826104f59..cbb9fb4eb 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -215,6 +215,7 @@ val fold_named_context_both_sides :
   ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a
 val mem_named_context : Id.t -> named_context -> bool
+val compact_named_context : named_context -> named_list_context
 
 val clear_named_body : Id.t -> env -> env
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 33bd5041e..75cce2755 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -304,10 +304,11 @@ 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 =
-    fold_named_context
-      (fun env d pps ->
-         let pidt =  pr_var_decl env sigma d in (pps ++ fnl () ++ pidt))
-      env ~init:(mt ())
+    Context.fold_named_list_context
+      (fun d pps ->
+         let pidt =  pr_var_list_decl env sigma d in
+         (pps ++ fnl () ++ pidt))
+      (Termops.compact_named_context (named_context env)) ~init:(mt ())
   in
   let db_env =
     fold_rel_context
@@ -330,16 +331,16 @@ let pr_context_limit n env sigma =
   else
     let k = lgsign-n in
     let _,sign_env =
-      fold_named_context
-        (fun env d (i,pps) ->
+      Context.fold_named_list_context
+        (fun d (i,pps) ->
            if i < k then
 	     (i+1, (pps ++str "."))
 	   else
-             let pidt = pr_var_decl env sigma d in
+             let pidt = pr_var_list_decl env sigma d in
 	     (i+1, (pps ++ fnl () ++
 		      str (emacs_str "") ++
 		      pidt)))
-        env ~init:(0,(mt ()))
+        (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ()))
     in
     let db_env =
       fold_rel_context