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".
---
 printing/printer.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index ed872afc67..7938b7bb0b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -219,7 +219,7 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
-let pr_var_decl env (id,c,typ) =
+let pr_var_decl_skel pr_id env (id,c,typ) =
   let pbody = match c with
     | None ->  (mt ())
     | Some c ->
@@ -231,6 +231,12 @@ let pr_var_decl env (id,c,typ) =
   let ptyp = (str" : " ++ pt) in
   (pr_id id ++ hov 0 (pbody ++ ptyp))
 
+let pr_var_decl env (id,c,typ) =
+  pr_var_decl_skel pr_id env (id,c,typ)
+
+let pr_var_list_decl env (l,c,typ) =
+  hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env (l,c,typ))
+
 let pr_rel_decl env (na,c,typ) =
   let pbody = match c with
     | None -> mt ()
-- 
cgit v1.2.3