aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-05 18:09:30 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-09-01 13:45:52 +0200
commit14e6dc5800a28d49dcdb714b06c02fced7b9fdaf (patch)
tree3e5e29685de4d9b9706ef01745305f2616c842e5 /kernel
parent9f7a633ae30f997c2e70c31681e92d1ef43f9655 (diff)
Coqide prints succesive hyps of the same type on 1 line
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
Diffstat (limited to 'kernel')
-rw-r--r--kernel/context.ml6
-rw-r--r--kernel/context.mli4
2 files changed, 9 insertions, 1 deletions
diff --git a/kernel/context.ml b/kernel/context.ml
index bdc4c067a..5256ee417 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 048edef95..1d732d273 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 *)