From 14e6dc5800a28d49dcdb714b06c02fced7b9fdaf Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 5 Aug 2014 18:09:30 +0200
Subject: Coqide prints succesive hyps of the same type on 1 line

This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
---
 kernel/context.ml  | 6 +++++-
 kernel/context.mli | 4 ++++
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/context.ml b/kernel/context.ml
index bdc4c067a6..5256ee4174 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -23,10 +23,13 @@ open Names
 (***************************************************************************)
 
 type named_declaration = Id.t * Constr.t option * Constr.t
+type named_list_declaration = Id.t list * Constr.t option * Constr.t
 type rel_declaration = Name.t * Constr.t option * Constr.t
 
-let map_named_declaration f (id, (v : Constr.t option), ty) =
+let map_named_declaration_skel f (id, (v : Constr.t option), ty) =
   (id, Option.map f v, f ty)
+let map_named_list_declaration = map_named_declaration_skel
+let map_named_declaration = map_named_declaration_skel
 
 let map_rel_declaration = map_named_declaration
 
@@ -77,6 +80,7 @@ let rel_context_nhyps hyps =
     goal assumptions. *)
 
 type named_context = named_declaration list
+type compacted_named_context = named_list_declaration list
 
 let empty_named_context = []
 
diff --git a/kernel/context.mli b/kernel/context.mli
index 048edef951..1d732d2732 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -19,10 +19,13 @@ open Names
     purpose) *)
 
 type named_declaration = Id.t * Constr.t option * Constr.t
+type named_list_declaration = Id.t list * Constr.t option * Constr.t
 type rel_declaration = Name.t * Constr.t option * Constr.t
 
 val map_named_declaration :
   (Constr.t -> Constr.t) -> named_declaration -> named_declaration
+val map_named_list_declaration :
+  (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
 val map_rel_declaration :
   (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
 
@@ -51,6 +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 rel_context = rel_declaration list
 (** In [rel_context], more recent declaration is on top *)
 
-- 
cgit v1.2.3