From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 3 May 2017 11:37:08 +0200
Subject: Adding an even more compact mode for goal display.

We want to print variables in vertical boxes as much as possible.

The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:

X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
---
 vernac/vernacentries.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2cb6f3918f..40cd1a29c9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1411,6 +1411,24 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
+let _ =
+  declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = Flags.print_hyps_limit;
+      optwrite = Flags.set_print_hyps_limit }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "display compact goal contexts";
+      optkey   = ["Printing";"Compact";"Contexts"];
+      optread  = (fun () -> Printer.get_compact_context());
+      optwrite = (fun b -> Printer.set_compact_context b) }
+
 let _ =
   declare_int_option
     { optsync  = true;
-- 
cgit v1.2.3


From 91d78c590b35c9edcf9f68c408ba82090f68e156 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 5 May 2017 12:59:41 +0200
Subject: Adapted to EConstr.

---
 vernac/vernacentries.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 40cd1a29c9..d4e6af9959 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1411,15 +1411,6 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
-let _ =
-  declare_int_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "the hypotheses limit";
-      optkey   = ["Hyps";"Limit"];
-      optread  = Flags.print_hyps_limit;
-      optwrite = Flags.set_print_hyps_limit }
-
 let _ =
   declare_bool_option
     { optsync  = true;
-- 
cgit v1.2.3


From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 Aug 2016 14:46:33 +0200
Subject: Uniformity of style for selecting plural or not; spacing for comma.

---
 vernac/obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0520216b2..5233fab151 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
-- 
cgit v1.2.3